Lemma is_precategory_relmodule (hs : has_homsets D) : is_precategory relmodule_precategory_data. 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.
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.