proposition: Lemma adj_after_nathomweq (H : are_adjoints F G) : adj_from_nathomweq (nathomweq_from_adj H) = H.
proof: 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.
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