proposition: Lemma fully_faithful_commutative_triangle_weq {C D : precategory} (F : functor C D) (fff : fully_faithful F) {X Y Z : ob C} (f : X --> Y) (g : Y --> Z) (h : X --> Z) : (f · g = h) ≃ (#F f · #F g = #F h).
proof: Proof. apply (@weqcomp _ (# F (f · g) = # F h)). - eapply make_weq. apply (isweqmaponpaths (weq_from_fully_faithful fff _ _) (f · g) h). - use weq_iso; intros p. + refine (_ @ p). apply (!functor_comp _ _ _). + refine (_ @ p). apply (functor_comp _ _ _). + refine (path_assoc _ _ _ @ _). refine (maponpaths (λ pp, pp @ _) (pathsinv0r _) @ _). reflexivity. + cbn. refine (path_assoc _ _ _ @ _). refine (maponpaths (λ pp, pp @ _) (pathsinv0l _) @ _). reflexivity. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence