Lemma are_conjugates_is_are_conjugates' {C C' D D' : category} {L : functor D C} {R : functor C D} {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' } (h : are_adjoints L R) (h' : are_adjoints L' R') (σ : DistrLaw L' L K H) (τ : DistrLaw K H R R') : are_conjugates h h' σ τ = are_conjugates' h h' σ τ. Proof. apply propositionalUnivalenceAxiom. - apply isaprop_are_conjugates. - apply isaprop_are_conjugates'. - red. intro P. red in P. intros A B g. set (hyp := (P A B (φ_adj_inv h g))). apply adjuncts_mutually_inverse2 in hyp. assert (hyp2 : # K (φ_adj h (φ_adj_inv h g)) = # K g). + apply maponpaths. apply φ_adj_after_φ_adj_inv. + apply pathsinv0 in hyp. eapply pathscomp0 in hyp. 2 : { apply maponpaths. apply cancel_postcomposition. apply pathsinv0. apply hyp2. } apply pathsinv0 in hyp. exact hyp. - red. intro P. red in P. intros A B f. set (hyp := (P A B (φ_adj h f))). apply (adjuncts_mutually_inverse1 h' (pr1 σ A · # H (φ_adj_inv h (φ_adj h f))) (# K (φ_adj h f) · pr1 τ B)) in hyp. eapply pathscomp0 in hyp. 2 : { apply maponpaths. apply cancel_precomposition. apply maponpaths. apply pathsinv0. apply φ_adj_inv_after_φ_adj. } exact hyp. 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.