proposition: 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: 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.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Adjunctions.Core