**********************************************************
Contents:
TODO:
• Proof that precategory_Monad C is univalent if C is (should follow easily from same result for relative monads RelativeMonads.is_univalent_RelMonad and isomorphism of categories with Kleisli triples KTriplesEquiv.is_catiso)
Written by: Benedikt Ahrens (started March 2015) Extended by: Anders Mörtberg, 2016 Extended by: Ralph Matthes, 2017 (Section MonadsUsingCoproducts)

Definition functor_with_μ (C : precategory_data) : UU
:= F : functor C C, F F F.

Coercion functor_from_functor_with_μ (C : precategory_data) (F : functor_with_μ C)
: functor C C := pr1 F.

Definition μ {C : precategory_data} (F : functor_with_μ C) : FF F := pr2 F.

Definition Monad_data (C : precategory_data) : UU :=
F : functor_with_μ C, functor_identity C F.

: functor_with_μ C := pr1 F.

Definition η {C : precategory_data} (F : Monad_data C)
: functor_identity C F := pr2 F.

Definition Monad_laws {C : precategory_data} (T : Monad_data C) : UU :=
(
( c : C, η T (T c) · μ T c = identity (T c))
×
( c : C, #T (η T c) · μ T c = identity (T c)))
×
( c : C, #T (μ T c) · μ T c = μ T (T c) · μ T c).

Lemma isaprop_Monad_laws (C : precategory_data) (hs : has_homsets C) (T : Monad_data C) :
Proof.
repeat apply isapropdirprod;
apply impred; intro c; apply hs.
Qed.

Lemma Monad_law1 {C : precategory_data} {T : Monad C} : c : C, η T (T c) · μ T c = identity (T c).
Proof.
exact (pr1 (pr1 (pr2 T))).
Qed.

Lemma Monad_law2 {C : precategory_data} {T : Monad C} : c : C, #T (η T c) · μ T c = identity (T c).
Proof.
exact (pr2 (pr1 (pr2 T))).
Qed.

Lemma Monad_law3 {C : precategory_data} {T : Monad C} : c : C, #T (μ T c) · μ T c = μ T (T c) · μ T c.
Proof.
exact (pr2 (pr2 T)).
Qed.

Definition Monad_Mor_laws {C : precategory_data} {T T' : Monad_data C} (α : T T')
: UU :=
( a : C, μ T a · α a = α (T a) · #T' (α a) · μ T' a) ×
( a : C, η T a · α a = η T' a).

Lemma isaprop_Monad_Mor_laws (C : precategory_data) (hs : has_homsets C)
(T T' : Monad_data C) (α : T T')
Proof.
apply isapropdirprod;
apply impred; intro c; apply hs.
Qed.

Definition Monad_Mor {C : precategory_data} (T T' : Monad_data C) : UU
:= α : T T', Monad_Mor_laws α.

: T T' := pr1 s.

: a : C, η T a · α a = η T' a.
Proof.
exact (pr2 (pr2 α)).
Qed.

: a : C, μ T a · α a = α (T a) · #T' (α a) · μ T' a.
Proof.
exact (pr1 (pr2 α)).
Qed.

Proof.
split; intros a; simpl.
- now rewrite id_left, id_right, functor_id, id_left.
- now apply id_right.
Qed.

(α : Monad_Mor T T') (α' : Monad_Mor T' T'') : Monad_Mor_laws (nat_trans_comp _ _ _ α α').
Proof.
split; intros; simpl.
- rewrite assoc.
set (H:=Monad_Mor_μ α a); simpl in H.
rewrite H; clear H; rewrite <- !assoc.
set (H:=Monad_Mor_μ α' a); simpl in H.
rewrite H; clear H.
rewrite functor_comp.
apply maponpaths.
now rewrite !assoc, nat_trans_ax.
- rewrite assoc.
Qed.

Definition Monad_Mor_equiv {C : precategory} (hs : has_homsets C)
: α = β (pr1 α = pr1 β).
Proof.
apply subtypeInjectivity; intro a.
Defined.

Definition precategory_Monad_ob_mor (C : precategory_data) : precategory_ob_mor.
Proof.
Defined.

Definition precategory_Monad_data (C : precategory) : precategory_data.
Proof.
Defined.

Lemma precategory_Monad_axioms (C : precategory) (hs : has_homsets C)
Proof.
repeat split; simpl; intros.
- apply (invmap (Monad_Mor_equiv hs _ _ )).
apply (@id_left (functor_precategory C C hs)).
- apply (invmap (Monad_Mor_equiv hs _ _ )).
apply (@id_right (functor_precategory C C hs)).
- apply (invmap (Monad_Mor_equiv hs _ _ )).
apply (@assoc (functor_precategory C C hs)).
- apply (invmap (Monad_Mor_equiv hs _ _ )).
apply (@assoc' (functor_precategory C C hs)).
Qed.

Definition precategory_Monad (C : precategory) (hs : has_homsets C) : precategory
:= tpair _ _ (precategory_Monad_axioms C hs).

Lemma has_homsets_precategory_Monad (C : precategory) (hs: has_homsets C) : has_homsets (precategory_Monad C hs).
Proof.
intros F G.
simpl.
apply isaset_total2 .
- apply isaset_nat_trans.
exact hs.
- intro m.
apply isasetaprop.
exact hs.
Qed.

Proof.
Qed.

Definition category_Monad (C : category) : category :=

Definition forgetfunctor_Monad (C : category) :
functor (category_Monad C) (functor_category C C).
Proof.
use make_functor.
- use make_functor_data.
+ exact (λ M, pr1 M: functor C C).
+ exact (λ M N f, pr1 f).
- abstract (split; red; intros; reflexivity).
Defined.

Proof.
intros M N.
apply isinclpr1.
apply homset_property.
Qed.

# Definition and lemmas for bind

Section bind.

Definition of bind
Definition bind {C : precategory_data} {T : Monad_data C} {a b : C} (f : Ca,T b) : CT a,T b := # T f · μ T b.

Context {C : precategory} {T : Monad C}.

Lemma η_bind {a b : C} (f : Ca,T b) : η T a · bind f = f.
Proof.
unfold bind.
rewrite assoc.
eapply pathscomp0;
[apply cancel_postcomposition, (! (nat_trans_ax (η T) _ _ f))|]; simpl.
rewrite <- assoc.
apply id_right.
Qed.

Lemma bind_η {a : C} : bind (η T a) = identity (T a).
Proof.
Qed.

Lemma bind_bind {a b c : C} (f : Ca,T b) (g : Cb,T c) :
bind f · bind g = bind (f · bind g).
Proof.
unfold bind; rewrite <- assoc.
eapply pathscomp0; [apply maponpaths; rewrite assoc;
apply cancel_postcomposition, (!nat_trans_ax (μ T) _ _ g)|].
rewrite !functor_comp, <- !assoc.
now apply maponpaths, maponpaths, (!Monad_law3 c).
Qed.

End bind.

# Operations for monads based on binary coproducts

Context {C : precategory} (T : Monad C) (BC : BinCoproducts C).

Local Notation "a ⊕ b" := (BinCoproductObject _ (BC a b)).

operation of weakening in a monad
Definition mweak (a b: C): CT b, T (a b) := bind (BinCoproductIn2 _ (BC _ _) · (η T _)).

operation of exchange in a monad
Definition mexch (a b c:C): CT (a (b c)), T (b (a c)).
Proof.
set (a1 := BinCoproductIn1 _ (BC _ _) · BinCoproductIn2 _ (BC _ _): Ca, b (a c)).
set (a21 := BinCoproductIn1 _ (BC _ _): Cb, b (a c)).
set (a22 := BinCoproductIn2 _ (BC _ _) · BinCoproductIn2 _ (BC _ _): Cc, b (a c)).
exact (bind ((BinCoproductArrow _ _ a1 (BinCoproductArrow _ _ a21 a22)) · (η T _))).
Defined.

Definition monadSubstGen {b:C} (a : C) (e : Cb,T a) : CT (b a), T a :=
bind (BinCoproductArrow _ _ e (η T a)).

Lemma subst_interchange_law_gen (c b a : C) (e : Cc,T (b a)) (f : Cb,T a):
(mexch c b a) · (monadSubstGen _ (f · (mweak c a)))
Proof.
do 3 rewrite bind_bind.
apply maponpaths.
apply BinCoproductArrowsEq.
+ do 4 rewrite assoc.
do 2 rewrite BinCoproductIn1Commutes.
rewrite <- assoc.
rewrite bind_bind.
rewrite <- assoc.
rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c a)) in pr1)).
rewrite <- assoc.
apply pathsinv0.
eapply pathscomp0.
× apply cancel_precomposition.
rewrite assoc.
rewrite BinCoproductIn2Commutes.
rewrite (η_bind(a:=(c a))).
apply idpath.
× now rewrite BinCoproductIn1Commutes.
+ rewrite assoc.
rewrite BinCoproductIn2Commutes.
rewrite (η_bind(a:=b a)).
do 3 rewrite assoc.
rewrite BinCoproductIn2Commutes.
apply BinCoproductArrowsEq.
× rewrite BinCoproductIn1Commutes.
rewrite <- assoc.
rewrite bind_bind.
do 2 rewrite assoc.
rewrite BinCoproductIn1Commutes.
rewrite <- assoc.
rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c a)) in pr1)).
rewrite assoc.
rewrite BinCoproductIn1Commutes.
unfold mweak.
rewrite <- assoc.
rewrite bind_bind.
apply pathsinv0.
apply remove_id_right; try now idtac.
rewrite <- bind_η.
apply maponpaths.
rewrite <- assoc.
rewrite (η_bind(a:=let (pr1, _) := pr1 (BC c a) in pr1)).
now rewrite BinCoproductIn2Commutes.
× rewrite BinCoproductIn2Commutes.
rewrite <- assoc.
rewrite bind_bind.
do 2 rewrite assoc.
rewrite BinCoproductIn2Commutes.
do 2 rewrite <- assoc.
rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c a)) in pr1)).
apply pathsinv0.
eapply pathscomp0.
- apply cancel_precomposition.
rewrite assoc.
rewrite BinCoproductIn2Commutes.
rewrite (η_bind(a:=(c a))).
apply idpath.
- now rewrite BinCoproductIn2Commutes.
Qed.

Context (TC : Terminal C).

Local Notation "1" := TC.

Definition monadSubst (a : C) (e : C1,T a) : CT (1 a), T a :=

Lemma subst_interchange_law (a : C) (e : C1,T (1 a)) (f : C1,T a):
(mexch 1 1 a) · (monadSubst _ (f · (mweak 1 a)))
Proof.
apply subst_interchange_law_gen.
Qed.

# Alternate (equivalent) definition of Monad

Definition raw_Monad_data (C : precategory_ob_mor) : UU :=
F : C C, ((( a b : ob C, a --> b F a --> F b) ×
( a : ob C, F (F a) --> F a)) ×
( a : ob C, a --> F a)).

functor_data C C := make_functor_data (pr1 T) (pr1 (pr1 (pr2 T))).

((is_functor T) ×
(is_nat_trans (functor_composite_data T T) T (pr2 (pr1 (pr2 T))))) ×
(is_nat_trans (functor_identity C) T (pr2 (pr2 T))).

(((_,, pr1 (pr1 (pr2 T))),,
(pr2 (pr1 (pr2 (pr1 T))),, (pr2 (pr1 (pr2 T))))),,
(pr2 (pr2 (pr1 T)),, (pr2 (pr2 T)))).

Proof.
use tpair.
- exact (functor_on_objects T).
- use tpair.
+ use tpair.
× exact (@functor_on_morphisms C C T).
× exact (μ T).
+ exact (η T).
Defined.

(Monad_to_raw_data T,, ((pr2 (T : functor C C),, (pr2 (μ T))),, pr2 (η T))).

Lemma Monad'_eq_raw_data {C : precategory} (hs : has_homsets C) (T T' : Monad' C) :
pr1 (pr1 T) = pr1 (pr1 T') T = T'.
Proof.
intro e.
apply subtypePath.
- apply subtypePath.
+ intro. apply isapropdirprod.
× apply isapropdirprod.
-- apply (isaprop_is_functor C C hs).
-- apply (isaprop_is_nat_trans C C hs).
× apply (isaprop_is_nat_trans C C hs).
+ apply e.
Qed.

Lemma Monad_eq_raw_data {C : precategory} (hs : has_homsets C) (T T' : Monad C) :
Proof.
intro e.
Qed.

Definition functor_with_μ_from_adjunction {C D : precategory}
{L : functor C D} {R : functor D C} (H : are_adjoints L R) :
functor_with_μ C.
Proof.
use tpair.
- exact (LR).
- exact (pre_whisker L (post_whisker (adjcounit H) R)).
Defined.

{R : functor D C} (H : are_adjoints L R) : Monad_data C.
Proof.
use tpair.
- cbn.
Defined.

{R : functor D C} (H : are_adjoints L R) : Monad C.
Proof.
use tpair.
- cbn.
use make_dirprod.
+ use make_dirprod.
× intro c; cbn.