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. use tpair. - apply (functor_composite (pr1 H2) (pr1 H1)). - apply are_adjoints_functor_composite. + apply (pr2 H1). + apply (pr2 H2). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.SplitMonicsAndEpis. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Section HomSetIsoRightFromPartial. End HomSetIsoRightFromPartial. Section HomSetIsoLeftFromPartial. End HomSetIsoLeftFromPartial.