proposition: Lemma monoid_to_disp_Monad_laws_CAT : disp_Monad_laws monoid_to_disp_Monad_data_CAT.
proof: Proof. repeat split. - intro c. set (t := monoid_right_unit_law _ M). exact (toforallpaths _ _ _ (base_paths _ _ t) c). - intro c. set (t := monoid_left_unit_law _ M). exact (toforallpaths _ _ _ (base_paths _ _ t) c). - intro c. set (t := monoid_assoc_law _ M). refine (! (toforallpaths _ _ _ (base_paths _ _ t) c) @ _). etrans. 1: apply assoc'. apply id_left. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.CategoryTheory.Monoidal.Examples.EndofunctorsMonoidalElementary UniMath.CategoryTheory.Monads.Monads