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. 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.
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.