Definition inv_relmonadmor_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 α) → category_RelMonad D J ⟦R', R⟧. Proof. intro T. set (fiso := (_,, T): z_iso(C := [C, D]) (R_functor R) (R_functor R')). set (finv := inv_from_z_iso fiso). exists (pr1 finv). unfold finv. split. - intros c. unfold fiso. etrans. { apply maponpaths, pathsinv0. apply (nat_trans_inv_pointwise_inv_after_p_z_iso C D D (R_functor R) (R_functor R')). } apply pathsinv0. apply z_iso_inv_on_left. simpl. apply pathsinv0. apply (r_eta_α (RelMonadMor_axioms_from_RelMonadMor α)). - intros a b f. unfold fiso. etrans. { apply cancel_postcomposition, pathsinv0. apply (nat_trans_inv_pointwise_inv_after_p_z_iso C D D (R_functor R) (R_functor R')). } etrans. { do 3 apply maponpaths. apply pathsinv0. apply (nat_trans_inv_pointwise_inv_after_p_z_iso C D D (R_functor R) (R_functor R')). } etrans. 2: { apply maponpaths. apply (nat_trans_inv_pointwise_inv_after_p_z_iso C D D (R_functor R) (R_functor R')). } apply z_iso_inv_on_left. rewrite <- assoc. apply pathsinv0. apply z_iso_inv_on_right. simpl. etrans. { apply pathsinv0. apply (α_r_bind (RelMonadMor_axioms_from_RelMonadMor α)). } apply cancel_precomposition. apply maponpaths. rewrite <- assoc. etrans. 2: { apply id_right. } apply cancel_precomposition. apply z_iso_inv_on_right. apply pathsinv0. apply id_right. 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.