proposition: Proposition isaprop_left_strength_laws {F : V ⟶ V} (tF : left_strength_data F) : isaprop (left_strength_laws tF).
proof: Proof. repeat (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