proposition: Lemma isaprop_RelModule_laws (hs : has_homsets D) (M : RelModule_data R) : isaprop (RelModule_laws M).
proof: Proof. apply isapropdirprod. - apply isaprop_RelMonad_axioms, hs. - apply isapropdirprod; repeat (apply impred; intros); apply hs. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.RelativeMonads