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. 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Adjunctions.Core.