{n : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    (map : {α β : TypeVec.{u} n} → α.Arrow β → F α → F β) →
      (P : MvPFunctor.{u} n) →
        (abs : {α : TypeVec.{u} n} → ↑P α → F α) →
          (repr : {α : TypeVec.{u} n} → F α → ↑P α) →
            (∀ {α : TypeVec.{u} n} (x : F α), abs (repr x) = x) →
              (∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (p : ↑P α), abs (MvFunctor.map f p) = map f (abs p)) → MvQPF F