Lemma is_nat_trans_τ_data_from_σ {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) : is_nat_trans _ _ (τ_data_from_σ h h' σ). Proof. red. intros c c' f. unfold τ_data_from_σ. etrans. { apply pathsinv0. simpl. apply φ_adj_natural_precomp. } apply pathsinv0. etrans. { apply pathsinv0. simpl. apply φ_adj_natural_postcomp. } apply maponpaths. etrans. 2: { set (Hσ := nat_trans_ax σ). change (# L' (# K (# R f))) with ( # (K ∙ L') (#R f)). rewrite assoc. apply cancel_postcomposition. apply pathsinv0. apply Hσ. } rewrite <- assoc. rewrite <- functor_comp. rewrite <- assoc. apply cancel_precomposition. change (# (L ∙ H) (# R f)) with (# H (# (R ∙ L) f)). etrans. 2: { apply (functor_comp H). } apply maponpaths. set (Hη := nat_trans_ax (counit_from_are_adjoints h)). apply pathsinv0. apply Hη. 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.