Lemma z_iso_from_is_relmonadmor_z_iso_idtoiso {C : precategory_data} (D : category) (J : functor C D) {R R': RelMonad J} (p : @paths (category_RelMonad D J) R R'): z_iso_from_is_relmonadmor_z_iso D J (idtoiso p) = idtoiso(C := [C, D]) (maponpaths (@R_functor C D J) p). Proof. unfold z_iso_from_is_relmonadmor_z_iso. simpl. apply (z_iso_eq(C := [C, D])). simpl. apply (nat_trans_eq D). intro c. induction p. apply idpath. 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.