Definition η_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 ⟦J c, x c⟧) (pr1_pr1_relmonadmor_eq_from_relmonadmor_z_iso H J α) (pr1 (pr2 (pr1 R))) = pr1 (pr2 (pr1 R')). Proof. apply funextsec; intro c. rewrite transport_of_relmonad_η_is_pointwise. unfold pr1_pr1_relmonadmor_eq_from_relmonadmor_z_iso. simpl. rewrite <- idtoiso_postcompose. simpl. change (pr1 (pr2 (pr1 R')) c) with (r_eta R' c). change (pr1 (pr2 (pr1 R)) c) with (r_eta R c). intermediate_path (r_eta R c · (pr1 (pr1 α): RelMonadMor_data _ _) c). 2: { set (X := RelMonadMor_axioms_from_RelMonadMor (pr1 α)). exact (pr1 X c). } apply cancel_precomposition. set (isor := z_iso_from_is_relmonadmor_z_iso D J α). set (isor_p := functor_z_iso_pointwise_if_z_iso' C D _ _ isor c). change (pr1 (pr1 α) c) with (pr1 isor_p). apply maponpaths. unfold precategory_data_from_precategory in isor. simpl in isor. unfold precategory_data_from_precategory; simpl. fold isor. intermediate_path (idtoiso (isotoid _ H isor_p)). 2: { apply idtoiso_isotoid. } apply maponpaths. 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). apply (isotoid_functorcat_pointwise C D H (R_functor R) (R_functor R')). 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.