Definition lift_μ : lift_functor ∙ lift_functor ⟹ lift_functor. Proof. use make_nat_trans. - intro X. cbn in X. exists (μ T X). abstract (red; cbn; rewrite functor_comp; rewrite <- assoc4; rewrite assoc; rewrite_cbn_inv (monad_dist_law3 l X); rewrite <- assoc; rewrite_cbn (nat_trans_ax (μ T) _ _ (Alg_map S X)); apply assoc). - abstract (intros X Y f; apply subtypePath; cbn; [ intro; apply homset_property | apply (nat_trans_ax (μ T))]). 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.