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