proposition: Lemma fg_pr2 : fg · π₂ = f2.
proof: Proof. unfold fg. refine (! homotinvweqweq (weq_from_fully_faithful Fw _ _) _ @ _). refine (_ @ homotinvweqweq (weq_from_fully_faithful Fw _ _) _). apply maponpaths. simpl. rewrite functor_comp. etrans. { apply maponpaths_2. apply (homotweqinvweq (weq_from_fully_faithful Fw _ _)). } exact (pr221 (Hp _ (#F f1) (#F f2))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.catiso UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecompEquivalence