proposition: Lemma is_left_adjoint_functor_composite {A B C : category} {F1 : functor A B} {F2 : functor B C} (H1 : is_left_adjoint F1) (H2 : is_left_adjoint F2) : is_left_adjoint (functor_composite F1 F2).
proof: Proof. use tpair. - apply (functor_composite (pr1 H2) (pr1 H1)). - apply are_adjoints_functor_composite. + apply (pr2 H1). + apply (pr2 H2). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Monics UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering