Definition lift_η : functor_identity (MonadAlg S) ⟹ lift_functor. Proof. use make_nat_trans. - intro X. cbn in X. exists (η T X). abstract (red; cbn; rewrite assoc; rewrite_cbn (monad_dist_law2 l X); apply (nat_trans_ax (η T))). - 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.