Definition is_relmonadmor_z_iso_from_is_z_iso {C : precategory_data} (D : category) (J : functor C D) {R R': RelMonad J} (α : category_RelMonad D J ⟦R, R'⟧) : is_z_isomorphism(C := [C, D]) (nat_trans_RelMonadMor α) → is_z_isomorphism α. Proof. intro T. exists (inv_relmonadmor_from_is_z_iso D J α T). split; simpl. - apply RelMonadMor_equiv. + apply D. + simpl. set (aux := z_iso_inv_after_z_iso ((_,, T): z_iso(C := [C, D]) (R_functor R) (R_functor R'))). apply (maponpaths pr1) in aux. exact aux. - apply RelMonadMor_equiv. + apply D. + simpl. set (aux := z_iso_after_z_iso_inv ((_,, T): z_iso(C := [C, D]) (R_functor R) (R_functor R'))). apply (maponpaths pr1) in aux. exact aux. 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.