Definition RelModule_Mor_equiv (hs : has_homsets D) {M N : RelModule R} (φ ψ : RelModule_Mor M N) : φ = ψ ≃ (pr1 φ = pr1 ψ). Proof. apply subtypeInjectivity; intro a. apply isaprop_RelModule_Mor_laws, hs. Defined.
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.