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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.