Lean4
instance [MvQPF F] [∀ i, MvQPF <| G i] : MvQPF (Comp F G)
where
P := MvPFunctor.comp (P F) fun i ↦ P <| G i
abs := Comp.mk ∘ (map fun _ ↦ abs) ∘ abs ∘ MvPFunctor.comp.get
repr {α} := MvPFunctor.comp.mk ∘ repr ∘ (map fun i ↦ (repr : G i α → (fun i : Fin2 n ↦ Obj (P (G i)) α) i)) ∘ Comp.get
abs_repr := by
intros
simp +unfoldPartialApp only [Function.comp_def, comp.get_mk, abs_repr, map_map, TypeVec.comp, MvFunctor.id_map',
Comp.mk_get]
abs_map := by
intros
simp only [(· ∘ ·)]
rw [← abs_map]
simp +unfoldPartialApp only [comp.get_map, map_map, TypeVec.comp, abs_map, map_mk]