{n : ℕ} →
  {F : TypeVec.{u} n → Type u} →
    [q : MvQPF F] →
      {G : TypeVec.{u} n → Type u} →
        [inst : MvFunctor G] →
          {FG_abs : {α : TypeVec.{u} n} → F α → G α} →
            {FG_repr : {α : TypeVec.{u} n} → G α → F α} →
              (∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x) →
                (∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (x : F α),
                    FG_abs (MvFunctor.map f x) = MvFunctor.map f (FG_abs x)) →
                  MvQPF G