proposition: Lemma adjuncts_mutually_inverse2 {C D : category} {A : D} {B : C} {L : functor D C} {R : functor C D} (h : are_adjoints L R) (f : L A --> B) (g : A --> R B) : φ_adj h f = g -> f = φ_adj_inv h g.
proof: Proof. intro p. set (η := unit_from_are_adjoints h). set (ε := counit_from_are_adjoints h). set (triangle_left := triangle_id_left_ad h). unfold φ_adj_inv. assert (hyp : g = (φ_adj h f)). - apply pathsinv0. exact p. - rewrite hyp. unfold φ_adj. rewrite functor_comp. change ( # L (# R f)) with (# (R ∙ L) f). rewrite <- assoc. set (Hε := nat_trans_ax ε). apply pathsinv0. etrans. { apply cancel_precomposition. apply Hε. } rewrite <- id_left. rewrite assoc. apply cancel_postcomposition. exact (triangle_left A). Qed.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Adjunctions.Core