Definition right_adjoint_to_adjunction {C₁ C₂ : category} {R : C₁ ⟶ C₂} (HR : is_right_adjoint R) : adjunction C₂ C₁. Proof. use make_adjunction. - use make_adjunction_data. + exact (left_adjoint HR). + exact R. + exact (adjunit (pr2 HR)). + exact (adjcounit (pr2 HR)). - split. + exact (pr122 HR). + exact (pr222 HR). 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.