proposition: Lemma adjuncts_mutually_inverse1 {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) : f = φ_adj_inv h g -> φ_adj h f = g.
proof: Proof. intro p. set (η := unit_from_are_adjoints h). set (ε := counit_from_are_adjoints h). set (triangle_right := triangle_id_right_ad h). change (unit_from_are_adjoints h) with η in triangle_right. change (counit_from_are_adjoints h) with ε in triangle_right. unfold φ_adj. assert (hyp : f = (φ_adj_inv h g)). - exact p. - rewrite hyp. unfold φ_adj_inv. rewrite functor_comp. change (# R (# L g)) with (# (L ∙ R) g). rewrite assoc. set (Hη := nat_trans_ax η). etrans. { apply cancel_postcomposition. apply pathsinv0. apply Hη. } rewrite <- id_right. rewrite <- assoc. apply cancel_precomposition. exact (triangle_right B). 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