proposition: Lemma is_precategory_relmodule (hs : has_homsets D) : is_precategory relmodule_precategory_data.
proof: Proof. apply is_precategory_one_assoc_to_two. repeat split. - intros x y f. apply (invmap (RelModule_Mor_equiv hs _ _ )). apply funextsec; intros a. apply id_left. - intros x y f. apply (invmap (RelModule_Mor_equiv hs _ _ )). apply funextsec; intros a. apply id_right. - intros x y z w f g h. apply (invmap (RelModule_Mor_equiv hs _ _ )). apply funextsec. intros a. apply assoc. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.RelativeMonads