Definition bind_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') : transportf (fun x : ob C -> ob D => ∏ c d, D ⟦J c, x d⟧ → D ⟦x c, x d⟧) (pr1_pr1_relmonadmor_eq_from_relmonadmor_z_iso H J α) (pr2 (pr2 (pr1 R))) = pr2 (pr2 (pr1 R')). Proof. apply funextsec; intro c. apply funextsec; intro d. apply funextsec; intro f. rewrite transport_of_relmonad_bind_is_pointwise. unfold pr1_pr1_relmonadmor_eq_from_relmonadmor_z_iso. simpl. rewrite double_transport_idtoiso. rewrite <- assoc. set (isor := z_iso_from_is_relmonadmor_z_iso D J α). unfold precategory_data_from_precategory in isor. simpl in isor. unfold precategory_data_from_precategory; simpl. fold isor. change (functor_eq_from_functor_z_iso H (R_functor R) (R_functor R') isor) with (isotoid _ (is_univalent_functor_category C D H) isor). do 2 rewrite (isotoid_functorcat_pointwise C D H (R_functor R) (R_functor R')). do 2 rewrite idtoiso_isotoid. change (pr2 (pr2 (pr1 R')) c d f) with (r_bind R' f). change (pr2 (pr2 (pr1 R)) c d) with (r_bind(c:=c)(d:=d) R). rewrite (transportb_isotoid D H). do 2 rewrite <- (z_iso_from_is_relmonadmor_z_iso_inv_p D J α). rewrite <- (z_iso_from_is_relmonadmor_z_iso_p D J α). assert (aux := α_r_bind (RelMonadMor_axioms_from_RelMonadMor (inv_from_z_iso α)) c d f). etrans. { apply assoc. } etrans. { apply cancel_postcomposition. apply aux. } intermediate_path (r_bind R' f · identity _). 2: { apply id_right. } etrans. { apply pathsinv0. apply assoc. } apply cancel_precomposition. assert (aux2 := z_iso_after_z_iso_inv α). apply (maponpaths pr1) in aux2. apply toforallpaths in aux2. apply aux2. 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.