Lemma adj_after_nathomweq (H : are_adjoints F G) : adj_from_nathomweq (nathomweq_from_adj H) = H. Proof. apply subtypePath. - intro. apply isaprop_form_adjunction. - apply dirprod_paths; cbn. + apply (nat_trans_eq (homset_property C)). intro c. cbn. unfold φ_adj, unit_from_are_adjoints. rewrite functor_id. apply id_right. + apply (nat_trans_eq (homset_property D)). intro d. cbn. unfold φ_adj_inv, counit_from_are_adjoints. rewrite functor_id. apply id_left. 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.