Definition is_z_iso_from_is_relmonadmor_z_iso {C : precategory_data} (D : category) (J : functor C D) {R R': RelMonad J} (α : z_iso(C := category_RelMonad D J) R R') : is_z_isomorphism(C := [C, D]) (nat_trans_RelMonadMor (pr1 α)). Proof. set (H' := z_iso_inv_after_z_iso α). set (H'':= z_iso_after_z_iso_inv α). set (α' := inv_from_z_iso α). exists (nat_trans_RelMonadMor α'). split; simpl. - unfold α'. unfold R_functor. apply (nat_trans_eq D). set (aux := maponpaths pr1 H'). apply toforallpaths in aux. exact aux. - unfold α'. unfold R_functor. apply (nat_trans_eq D). set (aux := maponpaths pr1 H''). apply toforallpaths 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.