proposition: Lemma comp_full_and_faithful_is_full_and_faithful (C D E : precategory) (F : functor C D) (f_and_f_F : full_and_faithful F) (G : functor D E) (f_and_f_G : full_and_faithful G) : full_and_faithful (functor_composite F G).
proof: Proof. split. - apply comp_full_is_full; [apply (pr1 f_and_f_F)|apply (pr1 f_and_f_G)]. - apply comp_faithful_is_faithful; [apply (pr2 f_and_f_F)|apply (pr2 f_and_f_G)]. 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