Definition T_on_SAlg : Algebra S -> Algebra S. Proof. intro X. use tpair. - exists (T X). exact (a X · (# T) (Alg_map S X)). - abstract (split; cbn; [ rewrite assoc; rewrite <- functor_id; rewrite <- Algebra_idlaw; rewrite functor_comp; rewrite <- (monad_dist_law1 l); apply idpath | rewrite 2 assoc; rewrite functor_comp; rewrite assoc4; rewrite_cbn (nat_trans_ax a _ _ (Alg_map S X)); rewrite_cbn_inv (monad_dist_law4 l X); rewrite <- assoc4; rewrite <- assoc; rewrite <- functor_comp; rewrite_cbn (Algebra_multlaw S X); rewrite functor_comp; apply assoc]). Defined.
Require Import UniMath.Foundations.PartD. 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.Derivative.