Lemma σ_from_τ_is_conjugate {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') (hs : has_homsets C') (τ : DistrLaw K H R R') : are_conjugates' h h' (σ_from_τ h h' τ) τ. Proof. red. intros A B g. unfold σ_from_τ. simpl. unfold σ_data_from_τ. set (η := (unit_from_are_adjoints h)). etrans. { apply pathsinv0. apply φ_adj_inv_natural_postcomp. } apply maponpaths. set (Hτ := nat_trans_ax τ). etrans. { rewrite <- assoc. apply cancel_precomposition. apply pathsinv0. apply Hτ. } rewrite assoc. apply cancel_postcomposition. change (# (R ∙ K) (φ_adj_inv h g)) with (# K (# R (φ_adj_inv h g))). etrans. { apply pathsinv0. use functor_comp. } apply maponpaths. change (nat_trans_data_from_nat_trans η A · # R (φ_adj_inv h g)) with (φ_adj h (φ_adj_inv h g)). apply φ_adj_after_φ_adj_inv. 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.