Definition monad_to_comp_data {a : T ∙ S ⟹ S ∙ T} (l : monad_dist_laws a) : T ⟹ monad_comp l := post_whisker (η S) T. Local Lemma monad_to_comp_law1 {a : T ∙ S ⟹ S ∙ T} (l : monad_dist_laws a) : ∏ x : C, μ T x · #T (η S x) = #T (η S (T x)) · #T (#S (#T (η S x))) · (#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))). Proof. intro x. rewrite <- assoc. rewrite (assoc (# T (# S (# T ((η S) x))))). rewrite <- functor_comp. apply pathsinv0. etrans. { apply cancel_precomposition. apply cancel_postcomposition. apply maponpaths. apply (nat_trans_ax a). } rewrite functor_comp. rewrite !assoc. rewrite <- functor_comp. rewrite (monad_dist_law1 l). rewrite <- !assoc. rewrite <- (nat_trans_ax (μ T) (S (S x))). rewrite (assoc (# T (# T (# S ((η S) x))))). simpl. rewrite <- !functor_comp. etrans. { apply cancel_precomposition. apply cancel_postcomposition. do 2 apply maponpaths. apply Monad_law2. } rewrite !functor_id. rewrite id_left. now rewrite <- (nat_trans_ax (μ T) x). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.LModules.