Definition monad_comp_data {C : category} {S T : Monad C} (a : T ∙ S ⟹ S ∙ T) : disp_Monad_data (S ∙ T) := tpair _ (monad_comp_mu a) (monad_comp_eta a). Context {C : category} {S T : Monad C}. Local Lemma monad_comp_law1 {a : T ∙ S ⟹ S ∙ T} (l : monad_dist_laws a) : ∏ x : C, (η S (T (S x))) · (η T (S (T (S x)))) · (#T (a (S x)) · (μ T (S (S x)) · #T (μ S x))) = identity (T (S x)). Proof. intro x. rewrite <- assoc. rewrite !(assoc ((η T) (S (T (S x))))). rewrite <- (nat_trans_ax (η T) (S (T (S x)))). simpl. rewrite !assoc. etrans. { do 3 apply cancel_postcomposition. apply (monad_dist_law1 l). } rewrite <- (assoc (# T ((η S) (S x)))). etrans. { apply cancel_postcomposition. apply cancel_precomposition. apply (Monad_law1). } rewrite id_right. rewrite <- functor_comp. rewrite <- functor_id. now etrans; try apply maponpaths; try apply Monad_law1. 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.