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 L' L K H) : are_conjugates h h' σ (τ_from_σ h h' σ). Proof. red. intros A B g. unfold τ_from_σ; simpl. unfold τ_data_from_σ. set (ε := (counit_from_are_adjoints h)). etrans. 2: { apply φ_adj_natural_precomp. } apply maponpaths. etrans. 2: { set (Hσ := nat_trans_ax σ). rewrite assoc. apply cancel_postcomposition. apply pathsinv0. apply Hσ. } rewrite <- assoc. apply cancel_precomposition. change (# (L ∙ H) (φ_adj h g)) with (# H (# L (φ_adj h g))). etrans. 2: { apply (functor_comp H). } apply maponpaths. apply pathsinv0. apply φ_adj_inv_after_φ_adj. 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.