**********************************************************
Contents:
Reference:
Written by: Benedikt Ahrens (started May 2017) Extended by: Ralph Matthes (starting August 2018), in particular all on univalence

Context {C D : precategory_data} {J : functor_data C D}.

:= F : C D, ( c, D J c, F c)
× ( c d, D J c, F d D F c, F d).

Definition RelMonad_ob (R : RelMonad_data) (c : C) : D := pr1 R c.
Definition r_eta (R : RelMonad_data) c : D J c, R c := pr1 (pr2 R) c.
Definition r_bind (R : RelMonad_data) {c d} (f : DJ c, R d) : D R c, R d
:= pr2 (pr2 R) _ _ f.

:= ( c, r_bind R (r_eta R c) = identity _ )
× ( c d (f : DJ c, R d), r_eta R _ · r_bind R f = f)
× ( c d e (f : D J c, R d) (g : D J d, R e),
r_bind R f · r_bind R g = r_bind R (f · r_bind R g)).

Proof.
apply isapropdirprod.
- apply impred_isaprop; intros. apply hs.
- apply isapropdirprod; repeat (apply impred_isaprop; intros); apply hs.
Defined.

: c, r_bind R (r_eta R c) = identity _ := pr1 X.
: c d (f : DJ c, R d), r_eta R _ · r_bind R f = f := pr1 (pr2 X).
: c d e (f : D J c, R d) (g : D J d, R e),
r_bind R f · r_bind R g = r_bind R (f · r_bind R g)
:= pr2 (pr2 X).

pr1 R = pr1 R' R = R'.
Proof.
intro p.
apply (total2_paths_f p).
apply proofirrelevance.
exact hs.
Defined.

previous proof
pr1 R = pr1 R' R = R'.
Proof.
intro p.
apply subtypeInjectivity.
- intro R''.
exact hs.
- assumption.
Defined.

Definition r_lift (R : RelMonad_data) {c d : C} (f : c --> d) : R c --> R d
:= r_bind R (#J f · r_eta R _ ).

Definition is_functor_r_lift {C: precategory_data} {D: precategory} {J : functor C D} (R : RelMonad)
: is_functor (RelMonad_ob R,, @r_lift _ _ J R).
Proof.
split; [intro c | intros a b c f g]; cbn; unfold r_lift; cbn.
- etrans. apply maponpaths.
etrans. eapply (maponpaths (λ x, x · _ )). apply functor_id.
apply id_left.
apply (r_bind_r_eta R).
- etrans. 2: { eapply pathsinv0; apply (r_bind_r_bind R). }
apply maponpaths.
etrans.
apply map_on_two_paths. apply functor_comp. apply idpath.
etrans.
2: { etrans. 2: apply assoc.
eapply pathsinv0. apply maponpaths. apply (r_eta_r_bind R).
}
apply pathsinv0, assoc.
Defined.

Definition R_functor {C: precategory_data} {D: precategory} {J : functor C D}
(R : RelMonad): functor C D
:= _,, is_functor_r_lift(J:=J) R.

Definition is_nat_trans_r_eta {C: precategory_data} {D: precategory} {J : functor C D}(R : RelMonad)
: is_nat_trans J (R_functor R) (r_eta R).
Proof.
red.
intros c c' f.
unfold R_functor; simpl.
unfold r_lift; simpl.
apply pathsinv0.
apply (r_eta_r_bind R).
Defined.

Definition r_eta_nat_trans {C: precategory_data} {D: precategory} {J : functor C D}(R : RelMonad)
: nat_trans J (R_functor R) := _ ,, is_nat_trans_r_eta R.

Definition r_lift_r_bind {C: precategory_data} {D: precategory} {J : functor C D}(R : RelMonad)(a b c : C) (f : b --> c) (g : J a --> R b)
: r_bind R g · r_lift R f = r_bind R (g · r_lift R f).
Proof.
unfold r_lift.
rewrite <- (r_bind_r_bind R).
apply idpath.
Defined.

Definition r_bind_r_lift {C: precategory_data} {D: precategory} {J : functor C D}(R : RelMonad)(a b c : C) (f : J b --> R c) (g : a --> b)
: r_lift R g · r_bind R f = r_bind R (#J g · f).
Proof.
unfold r_lift.
rewrite (r_bind_r_bind R).
apply maponpaths.
rewrite <- assoc.
apply cancel_precomposition.
apply (r_eta_r_bind R).
Defined.

analogue of UniMath.CategoryTheory.functor_categories.functor_eq_eq_from_functor_ob_eq
{J : functor C D} (R R' : RelMonad J) (p q : R = R')
(H : base_paths _ _ (base_paths _ _ p) =
base_paths _ _ (base_paths _ _ q)) :
p = q.
Proof.
apply (invmaponpathsweq (total2_paths_equiv _ _ _ )); simpl.
assert (H' : base_paths _ _ p = base_paths _ _ q).
{ apply (invmaponpathsweq (total2_paths_equiv _ _ _ )); simpl.
apply (two_arg_paths_f H), uip.
apply isaset_dirprod.
- apply impred_isaset; intro c. apply hs.
- apply impred_isaset; intro c; apply impred_isaset; intro d; apply impred_isaset; intro f.
apply hs.
}
apply (two_arg_paths_f H'), uip, isasetaprop, isaprop_RelMonad_axioms, hs.
Defined.

Kleisli precategory associated to a relative monad
Section Kleisli_precat.

Context {C: precategory_data} {D : precategory} {J : functor_data C D}.

Definition Kleisli_precat_ob_mor (R : RelMonad_data J) : precategory_ob_mor :=
make_precategory_ob_mor (ob C) (λ c d, J c --> R d).

Definition Kleisli_precat_data (R : RelMonad_data J) : precategory_data :=
make_precategory_data (Kleisli_precat_ob_mor R) (λ c, r_eta R c)
(λ a b c f g, f · r_bind R g).

Lemma Kleisli_precat_is_precat (R : RelMonad J) : is_precategory (Kleisli_precat_data R).
Proof.
apply is_precategory_one_assoc_to_two.
do 2 try apply tpair;
try unfold compose; simpl.
- intros a b f.
apply (r_eta_r_bind R).
- intros a b f.
now rewrite (r_bind_r_eta R), id_right.
- intros a b c d f g h.
now rewrite <- assoc, (r_bind_r_bind R).
Qed.

Definition Kleisli_precat (R : RelMonad J) : precategory := (_,, Kleisli_precat_is_precat R).

End Kleisli_precat.

Kleisli category associated to a relative monad
Section Kleisli_cat.

Lemma Kleisli_precat_has_homsets {C : precategory_data} {D : category} {J : functor_data C D} (R : RelMonad J)
(hs : has_homsets D) : has_homsets (Kleisli_precat_data R).
Proof.
intros a b.
apply hs.
Defined.

Definition Kleisli_cat {C : precategory_data} {D : category} {J : functor_data C D} (R : RelMonad J)
: category := (Kleisli_precat R,, Kleisli_precat_has_homsets R (homset_property D)).

End Kleisli_cat.

Definition RelMonadMor_data {C D : precategory_data}
{J : functor_data C D} (R R' : RelMonad_data J): UU :=
a : C, R a --> R' a.

Definition RelMonadMor_axioms {C D : precategory_data}
{J : functor_data C D} {R R' : RelMonad_data J} (α : RelMonadMor_data R R') : UU
:= ( a : C, r_eta R a · α a = r_eta R' a) ×
( (a b : C) (f : DJ a,R b), α a · r_bind R' (f · α b) = (r_bind R f α b).

Lemma isaprop_RelMonadMor_axioms {C D : precategory_data}
{J : functor_data C D} {R R' : RelMonad_data J} (α : RelMonadMor_data R R')
(hs : has_homsets D) :
Proof.
apply isapropdirprod; repeat (apply impred_isaprop; intros); apply hs.
Defined.

Definition r_eta_α {C D : precategory_data} {J : functor_data C D}
: a : C, r_eta R a · α a = r_eta R' a := pr1 X.

Definition α_r_bind {C D : precategory_data} {J : functor_data C D}
: (a b : C) (f : DJ a,R b), α a · r_bind R' (f · α b) = (r_bind R f) · α b := pr2 X.

Definition RelMonadMor {C D : precategory_data} {J : functor_data C D}
(R R' : RelMonad_data J) : UU
{R R' : RelMonad_data J} (α : RelMonadMor R R') : RelMonadMor_data R R' := pr1 α.

Definition RelMonadMor_map {C D : precategory_data} {J : functor_data C D}
{R R' : RelMonad_data J} (f : RelMonadMor R R') (X : C)
: R X --> R' X
:= (f : RelMonadMor_data _ _ ) X.

Definition RelMonadMor_equiv {C D : precategory_data} (hs : has_homsets D)
{J : functor_data C D} {R R' : RelMonad_data J} (α β : RelMonadMor R R') :
α = β ((α: RelMonadMor_data R R') = β).
Proof.
apply subtypeInjectivity.
intro a.
exact hs.
Defined.

Definition is_nat_trans_RelMonadMor {C : precategory_data} {D: precategory} {J : functor C D}
is_nat_trans (R_functor R) (R_functor R') (α:RelMonadMor_data R R').
Proof.
red.
intros c c' f.
unfold R_functor; simpl. unfold r_lift; simpl.
rewrite <- (α_r_bind α).
rewrite <- assoc.
now rewrite (r_eta_α α).
Defined.

Definition nat_trans_RelMonadMor {C : precategory_data} {D: precategory} {J : functor C D}
nat_trans (R_functor R) (R_functor R') := _ ,, is_nat_trans_RelMonadMor α.

Lemma RelMonad_identity_laws {C : precategory_data} {D : precategory}
{J : functor_data C D} (R : RelMonad_data J):
RelMonadMor_axioms (λ a : C, identity (R a)).
Proof.
split; simpl; intros c.
- apply id_right.
- intros. do 2 rewrite id_right; apply id_left.
Defined.

Definition RelMonad_identity {C : precategory_data} {D : precategory}
{J : functor_data C D} (R : RelMonad_data J): RelMonadMor R R

Lemma RelMonad_composition_laws {C : precategory_data} {D : precategory}
{J : functor_data C D} {R R' R'' : RelMonad_data J}
RelMonadMor_axioms (λ a : C, (α : RelMonadMor_data R R') a · (α' : RelMonadMor_data R' R'') a).
Proof.
split; intros; simpl.
- rewrite assoc.
rewrite (r_eta_α α).
apply (r_eta_α α').
- intermediate_path ((α:RelMonadMor_data R R') a ·
r_bind R'' ((f · (α:RelMonadMor_data R R') b) ·
× now repeat rewrite assoc.
× rewrite (α_r_bind α').
rewrite assoc. rewrite (α_r_bind α).
apply pathsinv0. apply assoc.
Defined.

Definition RelMonad_composition {C : precategory_data} {D : precategory}
{J : functor_data C D} {R R' R'' : RelMonad_data J}

Definition precategory_RelMonad_ob_mor {C : precategory_data} {D : precategory}
(J : functor_data C D) : precategory_ob_mor :=

Definition precategory_RelMonad_data {C : precategory_data} {D : precategory}
(J : functor_data C D) : precategory_data.
Proof.
- intro R.
- intros R R' R'' α α'.
Defined.

Lemma precategory_RelMonad_axioms {C : precategory_data} {D : precategory}
(hs : has_homsets D) (J : functor_data C D) :
Proof.
repeat split; simpl; intros.
- apply (invmap (RelMonadMor_equiv hs _ _ )).
apply funextsec. intros x. apply id_left.
- apply (invmap (RelMonadMor_equiv hs _ _ )).
apply funextsec. intros x. apply id_right.
- apply (invmap (RelMonadMor_equiv hs _ _ )).
apply funextsec. intros x. apply assoc.
- apply (invmap (RelMonadMor_equiv hs _ _ )).
apply funextsec. intros x. apply assoc'.
Defined.

Definition precategory_RelMonad {C : precategory_data} {D : precategory}
(hs : has_homsets D) (J : functor_data C D): precategory :=

Lemma has_homsets_RelMonad {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor_data C D) :
Proof.
intros R R'. simpl. unfold RelMonadMor.
apply isaset_total2 .
- apply impred_isaset.
intro. apply hs.
- intro α.
apply isasetaprop.
apply hs.
Defined.

Definition category_RelMonad {C : precategory_data} (D : category)
(J : functor_data C D) : category :=

Definition forgetfunctor_RelMonad {C : precategory} (D : category)
(J : functor C D) :
functor (category_RelMonad D J) (functor_category C D).
Proof.
use make_functor.
- simpl.
use make_functor_data.
+ simpl.
exact (λ R : RelMonad J, R_functor R).
+ simpl. intros R R' α.
- split.
+ red. intros. simpl. apply nat_trans_eq.
× apply D.
× intros; apply idpath.
+ unfold functor_compax. simpl. intros R R' R'' α α'. apply nat_trans_eq.
× apply D.
× intro c. apply idpath.
Defined.

Lemma forgetRelMonad_faithful {C : precategory} (D : category)
(J : functor C D) : faithful (forgetfunctor_RelMonad D J).
Proof.
intros R R'. simpl.
apply isinclbetweensets.
- apply isaset_total2.
+ apply impred_isaset.
intros. apply D.
+ intros. apply isasetaprop. apply isaprop_RelMonadMor_axioms. apply D.
- apply isaset_nat_trans. apply D.
- intros α α' p.
+ apply D.
+ apply funextsec. intro c.
rewrite p.
apply idpath.
Defined.

Definition relmonadmor_weq_nat_trans_fails {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D)(R R': RelMonad J) :
(precategory_RelMonad hs J R, R') [C, D, hs] R_functor R, R_functor R'.
Proof.
use isweq_iso.
- intro α.
(nat_trans_data_from_nat_trans α).
split; intros.
Abort.

Definition relmonadmor_eq_type {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D)(R R': RelMonad J) : UU
:= p : iso (C := [C, D, hs]) (R_functor R) (R_functor R'),

Definition relmonadmor_ob_eq {C : precategory_data} {D : precategory} (H: is_univalent D)
(J : functor C D)(R R': RelMonad J) :
(R = R') relmonadmor_eq_type (pr2 H) J R R'.
Proof.
eapply weqcomp.
- apply total2_paths_equiv.
- set (H1 := make_weq _ (pr1 (is_univalent_functor_category C D H) (R_functor R) (R_functor R'))).
Abort.

better upstream
Definition functor_iso_pointwise_if_iso' (C : precategory_data) (C' : precategory)
(hs: has_homsets C')
(F G : ob [C, C',hs]) (α: iso F G) :
a : ob C,
iso (pr1 F a) (pr1 G a) :=
λ a, tpair _ _ (is_functor_iso_pointwise_if_iso C C' _ F G (pr1 α) (pr2 α) a).

Lemma idtoiso_functorcat_compute_pointwise' (C : precategory_data) (D : precategory)
(hs: has_homsets D) (F G : ob [C, D, hs])
(p : F = G) (a : ob C) :
functor_iso_pointwise_if_iso' C D _ F G (idtoiso p) a =
idtoiso
(toforallpaths (λ _ : ob C, D) (pr1 (pr1 F)) (pr1 (pr1 G))
(base_paths (pr1 F) (pr1 G) (base_paths F G p)) a).
Proof.
induction p.
apply eq_iso. apply idpath.
Qed.
end of better upstream
a rather trivial observation
Definition is_iso_from_is_relmonadmor_iso {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (α : iso(C := precategory_RelMonad hs J) R R')
: is_iso(C := [C, D, hs]) (nat_trans_RelMonadMor (pr1 α)).
Proof.
apply is_iso_from_is_z_iso.
set (H' := iso_inv_after_iso α).
set (H'':= iso_after_iso_inv α).
set (α' := inv_from_iso α).
split; simpl.
- unfold α'. unfold R_functor.
apply (nat_trans_eq hs).
set (aux := maponpaths pr1 H'). apply toforallpaths in aux.
exact aux.
- unfold α'. unfold R_functor.
apply (nat_trans_eq hs).
set (aux := maponpaths pr1 H''). apply toforallpaths in aux.
exact aux.
Defined.

its immediate consequence
Definition iso_from_is_relmonadmor_iso {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (α : iso(C := precategory_RelMonad hs J) R R')
: iso(C := [C, D, hs]) (R_functor R) (R_functor R').
Proof.
use (make_iso(C := [C, D, hs]) (nat_trans_RelMonadMor (pr1 α))).
Defined.

Corollary iso_from_is_relmonadmor_iso_p {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (α : iso(C := precategory_RelMonad hs J) R R') (c : C) :
pr1 (pr1 α) c =
functor_iso_pointwise_if_iso' C D
hs (R_functor R) (R_functor R') (iso_from_is_relmonadmor_iso
hs J α) c.
Proof.
apply idpath.
Defined.

Lemma iso_from_is_relmonadmor_iso_idtoiso {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (p : @paths (precategory_RelMonad hs J) R R'):
iso_from_is_relmonadmor_iso hs J (idtoiso p) =
idtoiso(C := [C, D, hs]) (maponpaths (@R_functor C D J) p).
Proof.
simpl.
apply eq_iso.
simpl.
apply nat_trans_eq.
- exact hs.
- intro c.
induction p.
apply idpath.
Qed.

Definition alternative_inv_to_relmonadmor_iso {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (α : iso(C := precategory_RelMonad hs J) R R')
: precategory_RelMonad hs J R', R.
Proof.
use tpair.
- intro c.
exact (inv_from_iso (functor_iso_pointwise_if_iso' C D
hs (R_functor R) (R_functor R') (iso_from_is_relmonadmor_iso
hs J α) c)).
- split.
+ intro c.
apply pathsinv0.
apply iso_inv_on_left.
apply pathsinv0.
+ intros c d f.
apply iso_inv_on_left.
rewrite <- assoc.
apply pathsinv0.
apply iso_inv_on_right.
intermediate_path (pr1 (pr1 α) c · r_bind R' ((f · (inv_from_iso
(functor_iso_pointwise_if_iso' C D hs (R_functor R)
(R_functor R') (iso_from_is_relmonadmor_iso hs J α) d) )) ·
(functor_iso_pointwise_if_iso' C D hs (R_functor R)
(R_functor R') (iso_from_is_relmonadmor_iso hs J α) d ))).
2: { apply cancel_precomposition.
apply maponpaths.
rewrite <- assoc.
rewrite iso_after_iso_inv.
apply id_right.
}
apply pathsinv0.
Defined.

Lemma alternative_inv_to_relmonadmor_iso_is_inv {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (α : iso(C := precategory_RelMonad hs J) R R'):
alternative_inv_to_relmonadmor_iso hs J α = inv_from_iso α.
Proof.
apply inv_iso_unique'.
unfold precomp_with.
- exact hs.
- apply funextsec.
intro c.
simpl.
apply pathsinv0.
apply iso_inv_on_left.
rewrite id_left.
intermediate_path (pr1 (pr1 α) c).
{ apply idpath. }
apply idpath.
Qed.

Corollary iso_from_is_relmonadmor_iso_inv_p {C : precategory_data} {D : precategory} (hs: has_homsets D)
(J : functor C D) {R R': RelMonad J} (α : iso(C := precategory_RelMonad hs J) R R') (c : C) :
pr1 (inv_from_iso α) c =
inv_from_iso (functor_iso_pointwise_if_iso' C D
hs (R_functor R) (R_functor R') (iso_from_is_relmonadmor_iso
hs J α) c).
Proof.
apply idpath.
Qed.

the other direction, first the inverse monad morphism
Definition inv_relmonadmor_from_is_iso {C : precategory_data} {D : precategory}
(hs: has_homsets D) (J : functor C D){R R': RelMonad J}
(α : precategory_RelMonad hs J R, R')
: is_iso(C := [C, D, hs]) (nat_trans_RelMonadMor α) precategory_RelMonad hs J R', R.
Proof.
intro T.
set (fiso := make_iso(C := [C, D, hs]) (nat_trans_RelMonadMor α) T).
set (finv := inv_from_iso fiso).
(pr1 finv).
unfold finv.
split.
- intros c.
unfold fiso.
rewrite <- nat_trans_inv_pointwise_inv_after_p.
apply pathsinv0.
apply iso_inv_on_left.
simpl.
apply pathsinv0.
- intros a b f.
unfold fiso.
do 2 rewrite <- nat_trans_inv_pointwise_inv_after_p.
apply iso_inv_on_left.
rewrite <- assoc.
apply pathsinv0.
apply iso_inv_on_right.
simpl.
etrans.
{ apply pathsinv0.
apply cancel_precomposition.
apply maponpaths.
rewrite <- assoc.
etrans.
2: { apply id_right. }
apply cancel_precomposition.
apply iso_inv_on_right.
apply pathsinv0.
apply id_right.
Defined.

verification that the proposed inverse monad morphism is suitable
Definition is_relmonadmor_iso_from_is_iso {C : precategory_data} {D : precategory}
(hs: has_homsets D) (J : functor C D) {R R': RelMonad J}
(α : precategory_RelMonad hs J R, R')
: is_iso(C := [C, D, hs]) (nat_trans_RelMonadMor α) is_iso α.
Proof.
intro T.
apply is_iso_from_is_z_iso.
split; simpl.
-
+ exact hs.
+ simpl.
set (aux := iso_inv_after_iso (make_iso(C := [C, D, hs]) (nat_trans_RelMonadMor α) T)).
apply (maponpaths pr1) in aux.
exact aux.
+ exact hs.
+ simpl.
set (aux := iso_after_iso_inv (make_iso(C := [C, D, hs]) (nat_trans_RelMonadMor α) T)).
apply (maponpaths pr1) in aux.
exact aux.
Defined.

its immediate consequence
Definition relmonadmor_iso_from_is_iso {C : precategory_data} {D : precategory}
(hs: has_homsets D) (J : functor C D)(R R': RelMonad J)
(α : precategory_RelMonad hs J R, R')
: is_iso(C := [C, D, hs]) (nat_trans_RelMonadMor α) iso(C := precategory_RelMonad hs J) R R'.
Proof.
intro T.
use (make_iso α).
exact (is_relmonadmor_iso_from_is_iso hs J α T).
Defined.

Definition relmonadmor_iso_first_iso {C : precategory_data} {D : precategory}
(hs: has_homsets D) (J : functor C D)(R R': RelMonad J)
: iso(C := precategory_RelMonad hs J) R R' α : R_functor R R_functor R', is_iso(C := [C, D, hs]) α.
Proof.
unfold iso.
Abort.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J} :
iso(C := precategory_RelMonad (pr2 H) J) R R' pr1 (pr1 R) = pr1 (pr1 R').
Proof.
intro α.
change (pr1 (pr1 (R_functor R)) = pr1 (pr1 (R_functor R'))).
do 2 apply maponpaths.
set (H1 := make_weq _ (pr1 (is_univalent_functor_category C D H) (R_functor R) (R_functor R'))).
apply H1.
apply (iso_from_is_relmonadmor_iso (pr2 H) J α).
Defined.

(hs: has_homsets D) (J : functor C D) {R R': RelMonad J}
(p: @paths (precategory_RelMonad hs J) R R'):
base_paths (pr1 (R_functor R)) (pr1 (R_functor R'))
(base_paths (R_functor R) (R_functor R') (maponpaths R_functor p)) =
base_paths (pr1 R) (pr1 R') (base_paths R R' p).
Proof.
unfold base_paths.
etrans.
{ apply maponpaths.
apply (maponpathscomp (@R_functor C D J) (@functor_data_from_functor C D)).
}
etrans.
{ apply (maponpathscomp ((functor_data_from_functor C D R_functor)%functions) (@functor_on_objects C D)). }
etrans.
2: { apply pathsinv0.
}
apply idpath.
Qed.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J}
(p: @paths (precategory_RelMonad (pr2 H) J) R R'):
base_paths (pr1 R) (pr1 R') (base_paths R R' p).
Proof.
simpl.
rewrite functor_eq_from_functor_iso_idtoiso.
Qed.

Lemma transport_of_relmonad_η_is_pointwise {C : precategory_data} {D : precategory}
(J : functor C D) (F0 G0 : ob C ob D)
(F1 : a : ob C, J a --> F0 a)
(gamma : F0 = G0 )
(c: ob C) :
transportf (fun x : ob C ob D a, D J a, x a) gamma F1 c =
transportf (fun d: ob DD J c, d) (toforallpaths (λ _ : ob C, D) F0 G0 gamma c) (F1 c).
Proof.
induction gamma.
apply idpath.
Defined.

Lemma transport_of_relmonad_bind_is_pointwise {C : precategory_data} {D : precategory}
(J : functor C D) (F0 G0 : ob C ob D)
(F1 : a b : ob C , D J a, F0 b D F0 a, F0 b)
(gamma : F0 = G0 )
(c d : ob C) (f : J c --> G0 d) :
transportf (fun x : ob C ob D a b : ob C , D J a, x b D x a, x b) gamma F1 c d f =
double_transport (toforallpaths (λ _ : ob C, D) F0 G0 gamma c)
(toforallpaths (λ _ : ob C, D) F0 G0 gamma d)
(F1 c d (transportb (fun x : ob DD J c, x)
(toforallpaths (λ _ : ob C, D) F0 G0 gamma d) f)).
Proof.
induction gamma.
apply idpath.
Defined.

a preparation for the following lemma
Lemma isotoid_functorcat_pointwise_aux (C : precategory_data) (D : precategory)
(H : is_univalent D) (F G : ob [C, D, (pr2 H)]) (p: F = G) (c: C) :
let α := idtoiso p in
toforallpaths (fun _ : ob Cob D) (pr1 (pr1 F)) (pr1 (pr1 G))
(maponpaths pr1
(maponpaths pr1
(isotoid [C, D, pr2 H]
(is_univalent_functor_category C D H) α))) c
= isotoid D H
(functor_iso_pointwise_if_iso C D (pr2 H) F G α (pr2 α) c).
Proof.
induction p.
cbn delta in ×.
unfold functor_iso_pointwise_if_iso.
rewrite isotoid_idtoiso.
unfold idtoiso.
simpl.
apply idtoiso_inj; try assumption.
rewrite idtoiso_isotoid.
simpl.
apply eq_iso.
apply idpath.
Defined.

general lemma on univalence of functor category
Lemma isotoid_functorcat_pointwise (C : precategory_data) (D : precategory) (H : is_univalent D)
(F G : ob [C, D, (pr2 H)]) (α: iso F G) (c: C) :
toforallpaths (fun _ : ob Cob D) (pr1 (pr1 F)) (pr1 (pr1 G))
(maponpaths pr1
(maponpaths pr1
(isotoid [C, D, pr2 H]
(is_univalent_functor_category C D H) α))) c
= isotoid D H
(functor_iso_pointwise_if_iso' C D (pr2 H) F G α c).
Proof.
assert (aux := isotoid_functorcat_pointwise_aux C D H F G
(isotoid [C, D, pr2 H] (is_univalent_functor_category C D H) α)).
rewrite idtoiso_isotoid in aux.
apply aux.
Qed.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J}
(α: iso(C := precategory_RelMonad (pr2 H) J) R R')
: transportf (fun x : ob C ob D c, D J c, x c)
pr1 (pr2 (pr1 R')).
Proof.
apply funextsec; intro c.
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).
exact (pr1 X c).
}
apply cancel_precomposition.
set (isor := iso_from_is_relmonadmor_iso (pr2 H) J α).
set (isor_p := functor_iso_pointwise_if_iso' C D (pr2 H) _ _ 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_iso
(pr2 H) 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.

the following lemma should also be put upstream
Lemma transportb_isotoid (C : precategory) (H : is_univalent C)
(a b b' : ob C) (p : iso b b') (f : a --> b') :
transportb (λ b0 : C, a --> b0) (isotoid C H p) f = f · inv_from_iso p.
Proof.
apply pathsinv0.
apply transportb_transpose_right.
change (precategory_morphisms a) with (λ b0 : C, a --> b0).
rewrite transportf_isotoid'.
rewrite <- assoc.
rewrite iso_after_iso_inv.
apply id_right.
Qed.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J}
(α: iso(C := precategory_RelMonad (pr2 H) J) R R')
: transportf (fun x : ob C ob D c d, D J c, x d D x c, x d)
pr2 (pr2 (pr1 R')).
Proof.
apply funextsec; intro c. apply funextsec; intro d. apply funextsec; intro f.
simpl.
rewrite double_transport_idtoiso.
rewrite <- assoc.
set (isor := iso_from_is_relmonadmor_iso (pr2 H) J α).
unfold precategory_data_from_precategory in isor.
simpl in isor.
unfold precategory_data_from_precategory; simpl.
fold isor.
change (functor_eq_from_functor_iso
(pr2 H) 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 <- (iso_from_is_relmonadmor_iso_inv_p (pr2 H) J α).
rewrite <- (iso_from_is_relmonadmor_iso_p (pr2 H) J α).
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 := iso_after_iso_inv α).
apply (maponpaths pr1) in aux2.
apply toforallpaths in aux2.
apply aux2.
Defined.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J}
(α : iso(C := precategory_RelMonad (pr2 H) J) R R')
: R = R'.
Proof.
- exact (pr2 H).
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 Fdirprod_pr1(X := c : C, D J c, F c )(Y := c d : C, D J c, F d D F c, F d ))). }
+ 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 Fdirprod_pr2(X := c : C, D J c, F c )(Y := c d : C, D J c, F d D F c, F d ))). }
Defined.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J}
(α : iso(C := precategory_RelMonad (pr2 H) J) R R')
: R = R'.
Proof.
fold Hob in η_eq, bind_eq.
induction R as [[F [e b]] a].
induction R' as [[F' [e' b']] a'].
simpl in Hob.
induction Hob.
cbn in η_eq, bind_eq.
+ exact (pr2 H).
+ simpl.
apply maponpaths.
apply pathsdirprod; assumption.
Defined.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J} (p: R = R') :
Proof.
- apply (pr2 H).
rewrite base_total2_paths.
rewrite base_total2_paths.
Qed.

(H: is_univalent D) (J : functor C D) {R R': RelMonad J}
(α : iso(C := precategory_RelMonad (pr2 H) J) R R') :
Proof.
apply eq_iso.
- exact (pr2 H).
-
apply funextsec; intro c.
etrans.
rewrite idtoiso_functorcat_compute_pointwise'.
rewrite base_total2_paths.
rewrite base_total2_paths.
intermediate_path (pr1 (idtoiso
(isotoid D H (functor_iso_pointwise_if_iso' C D (pr2 H) _ _ (iso_from_is_relmonadmor_iso (pr2 H) J α) c)))).
2: { rewrite idtoiso_isotoid.
apply idpath.
}
apply maponpaths.
apply maponpaths.
apply isotoid_functorcat_pointwise.
Qed.

Definition relmonadmor_idtoiso {C : precategory_data} {D : precategory}
(H: is_univalent D) (J : functor C D)(R R': RelMonad J) :
(R = R') iso(C := precategory_RelMonad (pr2 H) J) R R'.
Proof.
apply (make_weq (@idtoiso (precategory_RelMonad (pr2 H) J) R R')).
use isweq_iso.
Defined.

Lemma isweq_idtoiso_RelMonad {C : precategory_data} {D : precategory}
(H: is_univalent D) (J : functor C D)(R R': RelMonad J)
: isweq (@idtoiso (precategory_RelMonad (pr2 H) J) R R').
Proof.
apply (isweqhomot (relmonadmor_idtoiso H J R R')).
- intro p. induction p.
apply idpath.
- apply (pr2 _ ).
Qed.

Lemma is_univalent_RelMonad {C : precategory_data} {D : precategory}
(H: is_univalent D) (J : functor C D)(R R': RelMonad J)
: is_univalent (precategory_RelMonad (pr2 H) J).
Proof.
split.
- clear R R'. intros R R'.
Defined.

The canonical relative adjunction between J and the Kleisli category of a J-relative monad
This is the obvious generalization of the material in UniMath.CategoryTheory.Monads.KleisliCategory.

Definition Left_rKleisli_functor_data {C: precategory_data} {D : precategory}
{J : functor_data C D} (R: RelMonad J) :
functor_data C (Kleisli_precat R).
Proof.
use make_functor_data.
- apply idfun.
- intros a b f; unfold idfun.
exact (#J f · (r_eta R) b).
Defined.

Lemma Left_rKleisli_is_functor {C: precategory_data} {D : precategory}
{J : functor C D} (R: RelMonad J) :
is_functor (Left_rKleisli_functor_data R).
Proof.
split.
- intro a.
unfold Left_rKleisli_functor_data; simpl.
rewrite functor_id.
apply id_left.
- intros a b c f g.
unfold Left_rKleisli_functor_data; simpl.
unfold compose at 3; simpl.
rewrite functor_comp.
do 2 (rewrite <- assoc).
apply cancel_precomposition.
apply pathsinv0.
apply (r_eta_r_bind R).
Defined.

Definition Left_rKleisli_functor {C: precategory_data} {D : precategory}
{J : functor C D} (R: RelMonad J) :
functor C (Kleisli_precat R)
:= (Left_rKleisli_functor_data R,,Left_rKleisli_is_functor R).

Definition Right_rKleisli_functor_data {C: precategory_data} {D : precategory}
{J : functor_data C D} (R: RelMonad J):
functor_data (Kleisli_precat R) D.
Proof.
use make_functor_data.
- exact R.
- intros a b.
apply r_bind.
Defined.

Lemma Right_rKleisli_is_functor {C: precategory_data} {D : precategory}
{J : functor C D} (R: RelMonad J) :
is_functor (Right_rKleisli_functor_data R).
Proof.
use tpair.
- intro a.
unfold Right_rKleisli_functor_data; unfold identity;
unfold functor_on_morphisms; simpl.
apply (r_bind_r_eta R).
- intros a b c f g; simpl.
apply pathsinv0.
apply (r_bind_r_bind R).
Defined.

Definition Right_rKleisli_functor {C: precategory_data} {D : precategory}
{J : functor C D} (R: RelMonad J) :
functor (Kleisli_precat R) D
:= (Right_rKleisli_functor_data R,,Right_rKleisli_is_functor R).

Composition of the left and right Kleisli functors is equal to R as a functor

Definition rKleisli_functor_left_right_compose {C: precategory} {D : precategory}
(hs : has_homsets D) {J : functor C D} (R: RelMonad J) :
(Left_rKleisli_functor R) (Right_rKleisli_functor R) = R_functor R.
Proof.
use functor_eq.
- exact hs.
- use functor_data_eq_from_nat_trans.
+ intro a; apply idpath.
+ intros a b f; simpl.
rewrite id_right.
rewrite id_left.
apply idpath.
Defined.

Showing that these functors are relative adjoints

Definition rKleisli_functors_are_relative_adjoints {C: precategory_data} {D : precategory}
(hs : has_homsets D) {J : functor C D} (R: RelMonad J) :
are_relative_adjoints J (Left_rKleisli_functor R) (Right_rKleisli_functor R).
Proof.
use tpair.
- intros a b.
use tpair.
+ simpl.
apply idfun.
+ simpl.
apply idisweq.
- unfold idfun; split.
+ intros a b f c h.
simpl.
unfold compose at 1; simpl.
rewrite <- assoc.
apply cancel_precomposition.
apply (r_eta_r_bind R).
+ intros a b f c k; simpl.
reflexivity.
Defined.