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. 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.
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.