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