proposition: Lemma fully_faithful_inv_comp (C D : precategory_data) (F : functor C D) (FF : fully_faithful F) (a b c : ob C) (f : F a --> F b) (g : F b --> F c) : FF^-1 (f · g) = FF^-1 f · FF^-1 g.
proof: Proof. apply (invmaponpathsweq (weq_from_fully_faithful FF a c)). set (HFFac := homotweqinvweq (weq_from_fully_faithful FF a c) (f · g)). unfold fully_faithful_inv_hom. simpl in *. rewrite HFFac; clear HFFac. rewrite functor_comp. set (HFFab := homotweqinvweq (weq_from_fully_faithful FF a b) f). set (HFFbc := homotweqinvweq (weq_from_fully_faithful FF b c) g). simpl in *. rewrite HFFab; clear HFFab. rewrite HFFbc; clear HFFbc. apply idpath. 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