proposition: Proposition isaprop_left_strong_monad_laws {M : Monad V} (tM : left_strength M) : isaprop (left_strong_monad_laws tM).
proof: Proof. use isapropdirprod ; repeat (use impred ; intro) ; apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monoidal.Categories