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