Definition pr1_pr1_relmonadmor_eq_from_relmonadmor_z_iso {C : precategory_data} {D : category} (H: is_univalent D) (J : functor C D) {R R': RelMonad J} : z_iso(C := category_RelMonad D J) R R' -> pr1 (pr1 R) = pr1 (pr1 R'). Proof. intro α. change (pr1 (pr1 (R_functor R)) = pr1 (pr1 (R_functor R'))). do 2 apply maponpaths. set (H1 := make_weq _ ((is_univalent_functor_category C D H) (R_functor R) (R_functor R'))). apply H1. apply (z_iso_from_is_relmonadmor_z_iso D 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.