Definition relmonad_eq_eq_from_relmonad_ob_eq {C: precategory_data} {D: precategory} (hs: has_homsets D) {J : functor C D} (R R' : RelMonad J) (p q : R = R') (H : base_paths _ _ (base_paths _ _ p) = base_paths _ _ (base_paths _ _ q)) : p = q. Proof. apply (invmaponpathsweq (total2_paths_equiv _ _ _ )); simpl. assert (H' : base_paths _ _ p = base_paths _ _ q). { apply (invmaponpathsweq (total2_paths_equiv _ _ _ )); simpl. apply (two_arg_paths_f H), uip. apply isaset_dirprod. - apply impred_isaset; intro c. apply hs. - apply impred_isaset; intro c; apply impred_isaset; intro d; apply impred_isaset; intro f. apply hs. } apply (two_arg_paths_f H'), uip, isasetaprop, isaprop_RelMonad_axioms, hs. 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.