feat: transport an MvQPF instance along an equivalence (#10806)

This is code ported from [alexkeizer/QpfTypes](https://github.com/alexkeizer/QpfTypes).
It's primary use is to show that existing type functions which are equivalent to polynomial functors but not defined as such (e.g., `Sum`, `Prod`, etc.) are QPFs.

Mathlib/Control/Functor/Multivariate.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Simon Hudon
 -/
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Data.TypeVec
+import Mathlib.Logic.Equiv.Defs
 
 #align_import control.functor.multivariate from "leanprover-community/mathlib"@"008205aa645b3f194c1da47025c5f110c8406eab"
 
@@ -242,4 +243,9 @@ theorem LiftR_RelLast_iff (x y : F (α ::: β)) :
 
 end LiftPLastPredIff
 
+/-- Any type function that is (extensionally) equivalent to a functor, is itself a functor -/
+def ofEquiv {F F' : TypeVec.{u} n → Type*} [MvFunctor F'] (eqv : ∀ α, F α ≃ F' α) :
+    MvFunctor F where
+  map f x := (eqv _).symm <| f <$$> eqv _ x
+
 end MvFunctor

Mathlib/Data/QPF/Multivariate/Basic.lean

@@ -283,4 +283,17 @@ theorem liftpPreservation_iff_uniform : q.LiftPPreservation ↔ q.IsUniform := b
   rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]
 #align mvqpf.liftp_preservation_iff_uniform MvQPF.liftpPreservation_iff_uniform
 
+/-- Any type function `F` that is (extensionally) equivalent to a QPF, is itself a QPF,
+assuming that the functorial map of `F` behaves similar to `MvFunctor.ofEquiv eqv` -/
+def ofEquiv {F F' : TypeVec.{u} n → Type*} [MvFunctor F'] [q : MvQPF F'] [MvFunctor F]
+    (eqv : ∀ α, F α ≃ F' α)
+    (map_eq : ∀ (α β : TypeVec n) (f : α ⟹ β) (a : F α),
+      f <$$> a = ((eqv _).symm <| f <$$> eqv _ a) := by intros; rfl) :
+    MvQPF F where
+  P         := q.P
+  abs α     := (eqv _).symm <| q.abs α
+  repr α    := q.repr <| eqv _ α
+  abs_repr  := by simp [q.abs_repr]
+  abs_map   := by simp [q.abs_map, map_eq]
+
 end MvQPF