feat: show that every polynomial functor is a (trivial) QPF (#10807)

Every polynomial functor `P` is trivially also a quotient of a polynomial functor, namely, it's a quotient of itself through equality. That is, `abs` and `repr` are just the identity.

Mathlib/Data/QPF/Multivariate/Basic.lean

@@ -297,3 +297,11 @@ def ofEquiv {F F' : TypeVec.{u} n → Type*} [MvFunctor F'] [q : MvQPF F'] [MvFu
   abs_map   := by simp [q.abs_map, map_eq]
 
 end MvQPF
+
+/-- Every polynomial functor is a (trivial) QPF -/
+instance MvPFunctor.instMvQPFObj {n} (P : MvPFunctor n) : MvQPF P where
+  P := P
+  abs := id
+  repr := id
+  abs_repr := by intros; rfl
+  abs_map := by intros; rfl