Definition relmonad_eq_from_relmonad_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') : R = R'. Proof. apply RelMonad_eq. - exact D. - set (Hob := pr1_pr1_relmonadmor_eq_from_relmonadmor_z_iso H J α). apply (total2_paths_f Hob). apply dirprodeq. + intermediate_path (transportf (λ F : C → D, ∏ c : C, D ⟦ J c, F c ⟧) Hob (pr1 (pr2 (pr1 R)))). { apply pathsinv0. apply (transport_map (fun F => dirprod_pr1(X := ∏ c : C, D ⟦ J c, F c ⟧)(Y := ∏ c d : C, D ⟦ J c, F d ⟧ → D ⟦ F c, F d ⟧))). } apply (η_relmonadmor_eq_from_relmonadmor_z_iso H J α). + intermediate_path (transportf (λ F : C → D, ∏ c d : C, D ⟦ J c, F d ⟧ → D ⟦ F c, F d ⟧) Hob (pr2 (pr2 (pr1 R)))). { apply pathsinv0. apply (transport_map (fun F => dirprod_pr2(X := ∏ c : C, D ⟦ J c, F c ⟧)(Y := ∏ c d : C, D ⟦ J c, F d ⟧ → D ⟦ F c, F d ⟧))). } apply (bind_relmonadmor_eq_from_relmonadmor_z_iso H J α). 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.