Definition relmonadmor_idtoiso {C : precategory_data} {D : category} (H: is_univalent D) (J : functor C D)(R R': RelMonad J) : (R = R') ≃ z_iso(C := category_RelMonad D J) R R'. Proof. apply (make_weq (@idtoiso (category_RelMonad D J) R R')). use isweq_iso. - exact (relmonad_eq_from_relmonad_z_iso H J). - intro p. exact (relmonad_eq_from_relmonad_z_iso_idtoiso H J p). - intro α. exact (idtoiso_relmonad_eq_from_relmonad_z_iso H J α). 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.