Lemma precategory_RelMonad_axioms {C : precategory_data} {D : precategory} (hs : has_homsets D) (J : functor_data C D) : is_precategory (precategory_RelMonad_data J). Proof. repeat split; simpl; intros. - apply (invmap (RelMonadMor_equiv hs _ _ )). apply funextsec. intros x. apply id_left. - apply (invmap (RelMonadMor_equiv hs _ _ )). apply funextsec. intros x. apply id_right. - apply (invmap (RelMonadMor_equiv hs _ _ )). apply funextsec. intros x. apply assoc. - apply (invmap (RelMonadMor_equiv hs _ _ )). apply funextsec. intros x. apply assoc'. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core.