Definition left_adjoint_to_adjunction {C₁ C₂ : category} {L : C₁ ⟶ C₂} (HL : is_left_adjoint L) : adjunction C₁ C₂. Proof. use make_adjunction. - use make_adjunction_data. + exact L. + exact (right_adjoint HL). + exact (adjunit HL). + exact (adjcounit HL). - split. + exact (pr122 HL). + exact (pr222 HL). 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.