Lemma comp_ff_is_ff (C D E : precategory) (F : functor C D) (ffF : fully_faithful F) (G : functor D E) (ffG : fully_faithful G) : fully_faithful (functor_composite F G). Proof. unfold fully_faithful in *. intros ? ?; apply (pr2 (weqcomp (_,, ffF _ _) (_,, ffG _ _))). 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.