Lemma isweq_idtoiso_RelMonad {C : precategory_data} {D : category} (H: is_univalent D) (J : functor C D)(R R': RelMonad J) : isweq (@idtoiso (category_RelMonad D J) R R'). Proof. apply (isweqhomot (relmonadmor_idtoiso H J R R')). - intro p. induction p. apply idpath. - apply (pr2 _ ). Qed.
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.