(** Basics of category theory. Category, monad, functor, natural transformation, adjunction, monad.

Uses axioms:
- extensional equality of functions;
- proof-irrelevance.

Does not use embedding of Haskell classes into Coq; Coq modules.

Notations. Every structure (e.g. functor) is divided into two parts: [x_set] and [x_prop]. [x_set] contains "data" and [x_prop] contains axioms/laws which data satisfies. We need this splitting when comparing structures using [sig_eq].
- ob = object
- mor = morphism
- id = identity morphism
- comp = composition of morphisms
- fr = functor
- nt = natural transformation
- md = monad
- adj = adjunction *)

Require Import Coq.Logic.ProofIrrelevance.
Require Beroal.Init.
Require Beroal.FunExtEq.

Set Implicit Arguments.

Definition sig_eq := Beroal.Init.sig_eq proof_irrelevance.
Definition fun_ext_eq := Beroal.FunExtEq.ext_eq_dep.

(** * Category *)

(** [category] does not containt a type of objects. Instead a type of objects is a parameter. Then we define functor category as [category], we do not need to duplicate [category] [Record]. *)
Record category (ob : Type) : Type :=
{ hom : ob -> ob -> Type
; id : forall ob1:ob, hom ob1 ob1
; comp : forall ob1 ob2 ob3:ob, hom ob2 ob3
	-> hom ob1 ob2 -> hom ob1 ob3
; id_left : forall (ob1 ob2:ob) (m:hom ob1 ob2),
	m = comp (id _) m
; id_right : forall (ob1 ob2:ob) (m:hom ob1 ob2),
	m = comp m (id _)
; comp_assoc : forall (ob1 ob2 ob3 ob4:ob)
	(m34: hom ob3 ob4) (m23: hom ob2 ob3) (m12: hom ob1 ob2),
	comp m34 (comp m23 m12)
	= comp (comp m34 m23) m12
}.

(** We need this [Record] to allow Coq automatically infer domain and codomain of a morphism. We can't use [hom]. *)
Record homi (cat : sigT category) (dom cod : projT1 cat) : Type
	:= {un_homi : hom (projT2 cat) dom cod}.
Section homi.
Variable (cat:sigT category).
Definition idi := fun (ob0:projT1 cat)
	=> Build_homi _ _ _ (id _ ob0).
Definition compi := fun (ob0 ob1 ob2:projT1 cat)
	(m12 : homi cat ob1 ob2) (m01 : homi cat ob0 ob1)
	=> Build_homi _ _ _ (comp _ _ _ _ (un_homi m12) (un_homi m01)).
End homi.

(** composition of morphisms *)
Notation "a * b" := (compi a b) (at level 40, left associativity).

Section homi_fact.
Variable (cat:sigT category).

Definition id_lefti : forall (ob0 ob1:projT1 cat) (m:homi cat ob0 ob1),
	m = idi _ _ * m.
Proof.
refine (fun ob0 ob1 m => _).
unfold idi, compi.
destruct m.
simpl.
refine (f_equal (Build_homi cat ob0 ob1) (id_left _ _ _ _)).
Qed.

Definition id_righti : forall (ob0 ob1:projT1 cat) (m:homi cat ob0 ob1),
	m = m * idi _ _.
Proof.
refine (fun ob0 ob1 m => _).
unfold idi, compi.
destruct m.
simpl.
refine (f_equal (Build_homi cat ob0 ob1) (id_right _ _ _ _)).
Qed.

Definition comp_associ : forall (ob0 ob1 ob2 ob3:projT1 cat)
	(m23: homi cat ob2 ob3) (m12: homi cat ob1 ob2)
		(m01: homi cat ob0 ob1),
	m23 * (m12 * m01) = (m23 * m12) * m01.
Proof.
refine (fun ob0 ob1 ob2 ob3 mi23 mi12 mi01 => _).
unfold idi, compi.
destruct mi23 as [m23].
destruct mi12 as [m12].
destruct mi01 as [m01].
simpl.
refine (f_equal (Build_homi cat ob0 ob3) (comp_assoc _ _ _ _ _ _ _ _)).
Qed.

End homi_fact.



(** * Functor *)

Section functor.
Variable (cat_dom cat_cod:sigT category).
Let ob_dom := projT1 cat_dom.
Let ob_cod := projT1 cat_cod.

Record functor_set:Type
:= { frs_ob : ob_dom -> ob_cod
; frs_mor : forall dom cod : ob_dom,
	homi cat_dom dom cod
	-> homi cat_cod (frs_ob dom) (frs_ob cod)
}.
Record functor_prop(fr0:functor_set):Prop
:= { frs_pres_id : forall ob0:ob_dom, idi _ _ = frs_mor fr0 (idi _ ob0)
; frs_pres_comp : forall (ob0 ob1 ob2:ob_dom)
	(m12:homi cat_dom ob1 ob2) (m01:homi cat_dom ob0 ob1),
	frs_mor fr0 m12 * frs_mor fr0 m01 = frs_mor fr0 (m12 * m01)
}.
Definition functor := sig functor_prop.

Section functor_proj.
Variable fr0:functor.
Definition fr_ob := frs_ob (proj1_sig fr0).
Definition fr_mor := frs_mor (proj1_sig fr0).
End functor_proj.



(** * Natural transformation *)

Section nt.
Variable fr0 fr1:functor.
Definition nt_set := forall obd:ob_dom,
	homi cat_cod (fr_ob fr0 obd) (fr_ob fr1 obd).
Definition nt_prop := fun nt0:nt_set
	=> forall (obd obc:ob_dom) (m:homi cat_dom obd obc),
	fr_mor fr1 m * nt0 obd = nt0 obc * fr_mor fr0 m.
Definition nt := sig nt_prop.

Section nt_proj.
Variable nt0:nt.
Definition ntf := proj1_sig nt0.
Definition nt_mor_comm := proj2_sig nt0.
End nt_proj.

Definition nt_eq_set := fun nt0 nt1 => ntf nt0 = ntf nt1.

End nt.

Section nt_id.
Variable fr0:functor.

Definition nt_id_set := (fun obd => idi cat_cod (fr_ob fr0 obd)
	) : nt_set fr0 fr0.

Definition nt_id_prop : nt_prop nt_id_set.
Proof.
unfold nt_prop.
refine (fun obd obc m => _).
refine (match id_righti _ in _=dep return dep = _
	with refl_equal => _ end).
refine (id_lefti _).
Qed.

Definition nt_id := (exist _ nt_id_set nt_id_prop
	) : nt fr0 fr0.

End nt_id.

Section nt_comp.

Variable (fr0 fr1 fr2:functor) .

Definition nt_comp_set := fun (nt12:nt_set fr1 fr2) (nt01:nt_set fr0 fr1)
	=> (fun obd => nt12 obd * nt01 obd
	) : nt_set fr0 fr2.

Variable (nt12:nt fr1 fr2) (nt01:nt fr0 fr1).

Definition nt_comp_prop : nt_prop (nt_comp_set (ntf nt12) (ntf nt01)).
Proof.
unfold nt_prop.
refine (fun obd obc m => _).
refine (match comp_associ _ _ _ in _=dep
	return _ = dep
	with refl_equal => _ end).
refine (match nt_mor_comm nt01 _ in _=dep
	return _ = _ * dep
	with refl_equal => _ end).
refine (match sym_eq (comp_associ _ _ _) in _=dep
	return _ = dep
	with refl_equal => _ end).
refine (match nt_mor_comm nt12 _ in _=dep
	return _ = dep * _
	with refl_equal => _ end).
refine (comp_associ _ _ _).
Qed.

Definition nt_comp := (exist _
	(nt_comp_set (ntf nt12) (ntf nt01)) nt_comp_prop
	) : nt fr0 fr2.

End nt_comp.

(** functor category *)
Definition fr_cat : category (functor).
Proof.
refine (Build_category nt nt_id nt_comp _ _ _).
refine (fun fr0 fr1 nt0 => _).
	refine (sig_eq _ _ _).
	destruct nt0 as [ntf0 nt_mor_comm0].
	simpl.
	refine (fun_ext_eq _ _ _ (fun obd => id_lefti (ntf0 obd))).
refine (fun fr0 fr1 nt0 => _).
	refine (sig_eq _ _ _).
	destruct nt0 as [ntf0 nt_mor_comm0].
	simpl.
	refine (fun_ext_eq _ _ _ (fun obd => id_righti (ntf0 obd))).
refine (fun fr0 fr1 fr2 fr3 nt23 nt12 nt01 => _).
	refine (sig_eq _ _ _).
		destruct nt23 as [ntf23 nt_mor_comm23].
		destruct nt12 as [ntf12 nt_mor_comm12].
		destruct nt01 as [ntf01 nt_mor_comm01].
	simpl.
	refine (fun_ext_eq _ _ _ (fun obd
		=> comp_associ (ntf23 obd) (ntf12 obd) (ntf01 obd))).
Qed.

(*
Definition nti := fun (fr0 fr1:functor) => homi (existT _ _ fr_cat) fr0 fr1.
Definition Build_nti := fun (fr0 fr1:functor) (nt01:nt fr0 fr1)
=> (Build_homi (existT _ _ fr_cat) _ _ nt01) : nti fr0 fr1.
*)

End functor.

Notation "a =@ b" := (nt_eq_set a b) (at level 70, no associativity).
Notation "a @ b" := (nt_comp a b) (at level 40, left associativity).
Notation "a @$ b" := (nt_comp_set a b) (at level 40, left associativity).

Section fr_id.
Variable cat0:sigT category.
Definition fr_id_set := (Build_functor_set (fun a=>a) (fun _ _ a=>a)
	) : functor_set cat0 cat0.
Definition fr_id_prop : functor_prop fr_id_set.
Proof.
refine (Build_functor_prop _ _ _).
simpl.
	refine (fun _ => refl_equal _).
simpl.
	refine (fun _ _ _ _ _ => refl_equal _).
Qed.
Definition fr_id := (exist _ fr_id_set fr_id_prop
	) : functor cat0 cat0.
End fr_id.

Section fr_comp.
Variable (cat0 cat1 cat2:sigT category).

Definition fr_comp_set := fun (fr12 : functor_set cat1 cat2)
	(fr01 : functor_set cat0 cat1)
	=> (Build_functor_set
		(fun a => frs_ob fr12 (frs_ob fr01 a))
		(fun _ _ a => frs_mor fr12 (frs_mor fr01 a))
	) : functor_set cat0 cat2.

Variable (fr12 : functor cat1 cat2) (fr01 : functor cat0 cat1).

Definition fr_comp_prop
	: functor_prop (fr_comp_set (proj1_sig fr12) (proj1_sig fr01)).
Proof.
refine (Build_functor_prop _ _ _).
simpl.
	refine (fun ob0 => _).
	refine (match frs_pres_id (proj2_sig fr01) _ in _=dep
		return _ = fr_mor _ dep
		with refl_equal => _ end).
	refine (frs_pres_id (proj2_sig fr12) _).
simpl.
	refine (fun ob0 ob1 ob2 m12 m01 => _).
	refine (match frs_pres_comp (proj2_sig fr01) _ _ in _=dep
		return _ = fr_mor _ dep
		with refl_equal => _ end).
	refine (frs_pres_comp (proj2_sig fr12) _ _).
Qed.

Definition fr_comp := (exist _
	(fr_comp_set (proj1_sig fr12) (proj1_sig fr01))
	fr_comp_prop
	) : functor cat0 cat2.

End fr_comp.

Notation "a # b" := (fr_comp a b) (at level 40, left associativity).
Notation "a #$ b" := (fr_comp_set a b) (at level 40, left associativity).

Section comp_nt_fr_ob.
Variable (cat0 cat1 cat2:sigT category) (fr0 fr1:functor cat1 cat2).

Definition comp_nt_fr_ob_set := fun (nt0:nt_set fr0 fr1)
	(fr2:functor cat0 cat1)
	=> (fun oba => nt0 (fr_ob fr2 oba)
	) : nt_set (fr0 # fr2) (fr1 # fr2).

Variable (nt0:nt fr0 fr1) (fr2:functor cat0 cat1).
Definition comp_nt_fr_ob_prop
	: nt_prop (comp_nt_fr_ob_set (ntf nt0) fr2).
Proof.
unfold nt_prop.
refine (fun obd obc m => _).
refine (let ntf0 := proj1_sig (nt0) in _).
change (fr_mor fr1 (fr_mor fr2 m) * ntf0 (fr_ob fr2 obd) =
	ntf0 (fr_ob fr2 obc) * fr_mor fr0 (fr_mor fr2 m)).
refine (nt_mor_comm (nt0) (fr_mor fr2 m)).
Qed.
Definition comp_nt_fr_ob := (exist _
	(comp_nt_fr_ob_set (ntf nt0) fr2)
	comp_nt_fr_ob_prop
	) : nt (fr0 # fr2) (fr1 # fr2).

End comp_nt_fr_ob.

Notation "a '> b" := (comp_nt_fr_ob a b)
	(at level 25, left associativity).
Notation "a >$ b" := (comp_nt_fr_ob_set a b)
	(at level 25, left associativity).

Section comp_nt_fr_mor.

Variable (cat0 cat1 cat2:sigT category)
	(fr0 fr1:functor cat0 cat1).
Definition comp_nt_fr_mor_set := fun (fr2:functor cat1 cat2)
	(nt0:nt_set fr0 fr1)
	=> (fun oba => fr_mor fr2 (nt0 oba)
	) : nt_set (fr2 # fr0) (fr2 # fr1).

Variable (fr2:functor cat1 cat2) (nt0:nt fr0 fr1).
Definition comp_nt_fr_mor_prop
	: nt_prop (comp_nt_fr_mor_set fr2 (ntf nt0)).
Proof.
unfold nt_prop.
refine (fun obd obc m => _).
refine (let ntf0 := proj1_sig (nt0) in _).
change (fr_mor fr2 (fr_mor fr1 m) * fr_mor fr2 (ntf0 obd) =
	fr_mor fr2 (ntf0 obc) * fr_mor fr2 (fr_mor fr0 m)).
refine (match sym_eq (frs_pres_comp (proj2_sig fr2) _ _) in _=dep
	return dep = _
	with refl_equal => _ end).
refine (match sym_eq (frs_pres_comp (proj2_sig fr2) _ _) in _=dep
	return _ = dep
	with refl_equal => _ end).
refine (f_equal _ (nt_mor_comm (nt0) m)).
Qed.

Definition comp_nt_fr_mor := (exist _
	(comp_nt_fr_mor_set fr2 (ntf nt0)) comp_nt_fr_mor_prop
	) : nt (fr2 # fr0) (fr2 # fr1).

End comp_nt_fr_mor.

Notation "a <' b" := (comp_nt_fr_mor a b)
	(at level 20, right associativity).
Notation "a <$ b" := (comp_nt_fr_mor_set a b)
	(at level 20, right associativity).



(** * Composition of NT-s and functors, facts *)

(*
Definition comp_nt_fr_ob_assoc : forall
	(cat0 cat1 cat2 cat3:sigT category)
	(fr01:functor cat0 cat1) (fr12:functor cat1 cat2)
	(fra frb:functor cat2 cat3)
	(ntab:nt fra frb),
	ntab '> (fr12 # fr01) = ntab '> fr12 '> fr01.
Proof.
refine (fun cat0 cat1 cat2 cat3 fr01 fr12 fra frb ntab => _).
refine (sig_eq _ _ _).
simpl.
refine (refl_equal _).
Qed.

Definition comp_nt_fr_mor_assoc
	: forall (cat0 cat1 cat2 cat3:sigT category)
	(fr12:functor cat1 cat2) (fr23:functor cat2 cat3)
	(fra frb:functor cat0 cat1) (nt0:nt fra frb),
	fr23 <' fr12 <' nt0 = (fr23 # fr12) <' nt0.
Proof.
refine (fun cat0 cat1 cat2 cat3 fr01 fr23 fra frb nt0 => _).
refine (sig_eq _ _ _).
simpl.
refine (refl_equal _).
Qed.

Definition comp_nt_fr_ob_distrib := fun
	(cat0 cat1 cat2:sigT category)
	(fr01:functor  cat0 cat1)
	(fra frb frc:functor  cat1 cat2)
	(ntab:nt fra frb) (ntbc:nt frb frc)
	=> (refl_equal _
	) : (ntbc @ ntab) '> fr01 = (ntbc '> fr01) @ (ntab '> fr01).
*)

Definition comp_nt_fr_mor_distrib_set
	: forall (cat0 cat1 cat2:sigT category)
	(fr12:functor cat1 cat2)
	(fra frb frc:functor cat0 cat1)
	(ntbc:nt_set frb frc) (ntab:nt_set fra frb),
	(fr12 <$ ntbc) @$ (fr12 <$ ntab) = fr12 <$ (ntbc @$ ntab).
Proof.
refine (fun cat0 cat1 cat2 fr12 fra frb frc ntbc ntab => _).
refine (fun_ext_eq _ _ _ (fun oba => 
		(frs_pres_comp (proj2_sig fr12)
		(ntbc oba) (ntab oba)))).
Qed.

(*
Definition comp_nt_fr_mor_distrib
	: forall (cat0 cat1 cat2:sigT category)
	(fr12:functor cat1 cat2)
	(fra frb frc:functor cat0 cat1)
	(ntbc:nt frb frc) (ntab:nt fra frb),
	(fr12 <' ntbc) @ (fr12 <' ntab) = fr12 <' (ntbc @ ntab).
Proof.
refine (fun cat0 cat1 cat2 fr12 fra frb frc ntbc ntab => _).
refine (sig_eq _ _ _).
simpl.
refine (fun_ext_eq _ _ _ (fun oba => 
		(frs_pres_comp (proj2_sig fr12)
		(ntf ntbc oba) (ntf ntab oba)))).
Qed.

Definition comp_nt_fr_ob_id : forall
	(cat0 cat1 cat2:sigT category)
	(fr12:functor cat1 cat2)
	(fr01:functor cat0 cat1),
	nt_id (fr12 # fr01) =  nt_id fr12 '> fr01.
Proof.
refine (fun _ _ _ _ _ => _).
refine (sig_eq _ _ _).
simpl.
refine (refl_equal _).
Qed.
*)

Definition comp_nt_fr_mor_set_id : forall
	(cat0 cat1 cat2:sigT category)
	(fr12:functor cat1 cat2)
	(fr01:functor cat0 cat1),
	nt_id_set (fr12 # fr01) = fr12 <$ nt_id_set fr01.
Proof.
refine (fun cat0 cat1 cat2 fr12 fr01 => _).
simpl.
refine (fun_ext_eq _ _ _
	(fun oba => (frs_pres_id (proj2_sig fr12) _))).
Qed.

Definition comp_nt_fr_mor_id : forall
	(cat0 cat1 cat2:sigT category)
	(fr12:functor cat1 cat2)
	(fr01:functor cat0 cat1),
	nt_id (fr12 # fr01) = fr12 <' nt_id fr01.
Proof.
refine (fun cat0 cat1 cat2 fr12 fr01 => _).
refine (sig_eq _ _ _).
simpl.
refine (fun_ext_eq _ _ _
	(fun oba => (frs_pres_id (proj2_sig fr12) _))).
Qed.

(*
Definition comp_nt_fr_assoc
	: forall (cat0 cat1 cat2 cat3:sigT category)
	(fr01:functor cat0 cat1) (fr23:functor cat2 cat3)
	(fra frb:functor cat1 cat2) (nt0:nt fra frb),
	(fr23 <' nt0) '> fr01 = fr23 <' (nt0 '> fr01).
Proof.
refine (fun cat0 cat1 cat2 cat3 fr01 fr23 fra frb nt0 => _).
refine (sig_eq _ _ _).
simpl.
refine (refl_equal _).
Qed.

Section nt_comp_assoc.
Variable (cat0 cat1:sigT category)
	(fra frb frc frd:functor cat0 cat1)
	(ntab:nt fra frb) (ntbc:nt frb frc) (ntcd:nt frc frd).
Check ((comp_assoc (fr_cat cat0 cat1) _ _ _ _ _ _ _)
	: ntcd @ (ntbc @ ntab) = (ntcd @ ntbc) @ ntab).
End nt_comp_assoc.
*)

(** NT-s commute in the definition of Godement multiplication = horizontal composition *)
Definition nt_comm : forall (cat0 cat1 cat2:sigT category)
	(A0 A1 : functor cat0 cat1)
	(A : nt A0 A1)
	(B0 B1 : functor cat1 cat2)
	(B : nt B0 B1),
	B1 <' A @ B '> A0 =@ B '> A1 @ B0 <' A.
Proof.
refine (fun cat0 cat1 cat2 A0 A1 A B0 B1 B => _).
unfold nt_eq_set.
simpl.
refine (fun_ext_eq _ _ _ _).
refine (fun ob0 => _).
unfold nt_comp_set, comp_nt_fr_mor_set, comp_nt_fr_ob_set.
refine (let p0 := nt_mor_comm B in _).
unfold nt_prop in p0.
refine (p0 _ _ (ntf A ob0)).
Qed.



(** auxilary *)
Definition frl := fun (cat0 cat1:sigT category) (fr:functor cat0 cat1)
	=> fr # fr_id _.

(** * Adjunction *)

Section adjunction.

(** Example. [cats] is a category of sets, [cata] is a category of algebraic systems with a fixed signature. F is a free functor, U is an underlying functor. ret = η, fold = ε. Example. [cata] is a category of monoids. F = [list]. On monoid ⟨[nat],[plus],[0]⟩ "fold" is usual folding of a [list nat] with [plus] and [0]. *)

Variable cats cata : sigT category.

Record adjunction_set:Type
	:= { adjsF : functor cats cata; adjsU : functor cata cats
	; adjs_ret : nt (fr_id _) (adjsU # adjsF)
	; adjs_fold : nt (adjsF # adjsU) (fr_id _)
	}.
Record adjunction_prop (s:adjunction_set) : Prop
	:= { adjs_nt_eq_u : nt_id (frl (adjsU s))
		=@ (adjsU s) <' (adjs_fold s) @ (adjs_ret s) '> (adjsU s)
	; adjs_nt_eq_f : nt_id (frl (adjsF s))
		=@ (adjs_fold s) '> (adjsF s) @ (adjsF s) <' (adjs_ret s)
	}.
Definition adjunction := sig adjunction_prop.

Section adjunction_proj.
Variable a:adjunction.
Definition adjF := adjsF (proj1_sig a).
Definition adjU := adjsU (proj1_sig a).
Definition adj_ret := adjs_ret (proj1_sig a).
Definition adj_fold := adjs_fold (proj1_sig a).
End adjunction_proj.

End adjunction.
Implicit Arguments Build_adjunction_set [cats cata].



(** * Monad *)

Section md.
Variable (cat:sigT category).

(** ret = η, join = μ *)
Record md_set:Type
	:= { mds_fr : functor cat cat
	; mds_ret : nt (fr_id _) (frl mds_fr)
	; mds_join : nt (mds_fr # mds_fr) (frl mds_fr)
	}.
Record md_prop (s:md_set) : Prop
	:= { mds_id_left : nt_id (frl (mds_fr s))
		=@ mds_join s @ (mds_ret s '> mds_fr s)
	; mds_id_right : nt_id (frl (mds_fr s))
		=@ mds_join s @ (mds_fr s <' mds_ret s)
	; mds_assoc : mds_join s @ (mds_join s '> mds_fr s)
		=@ mds_join s @ (mds_fr s <' mds_join s)
	}.
Definition md := sig md_prop.

Section md_proj.
Variable m:md.
Definition md_fr := mds_fr (proj1_sig m).
Definition md_ret := mds_ret (proj1_sig m).
Definition md_join := mds_join (proj1_sig m).
End md_proj.

(** ** Algebra over a monad *)

Section alg_md.
Variable m:md.
Record alg_md_set:Type
	:= { ams_ob : projT1 cat
	; ams_fold : homi cat (fr_ob (md_fr m) ams_ob) ams_ob
	}.
Record alg_md_prop (s:alg_md_set) : Prop
	:= { ams_unit : idi _ _ = ams_fold s * (ntf (md_ret m) (ams_ob s))
	; ams_assoc : ams_fold s * (ntf (md_join m) (ams_ob s))
		= ams_fold s * (fr_mor (md_fr m) (ams_fold s))
	}.
Definition alg_md := sig alg_md_prop.

End alg_md.

End md.
Implicit Arguments Build_md_set [cat].
Implicit Arguments Build_alg_md_set [cat].
Implicit Arguments Build_alg_md_prop [cat].

(** ⟨T C,μ C⟩ is an algebra over a monad *)

Section alg_join.
Variable (cat:sigT category) (m:md cat) (C:projT1 cat).

Definition alg_join_set := Build_alg_md_set m
	(fr_ob (md_fr m) C) (ntf (md_join m) C).

Definition alg_join_prop : alg_md_prop alg_join_set.
Proof.
refine (Build_alg_md_prop _ _ _ _).
simpl.
	refine (f_equal (fun f => f C) (mds_id_left (proj2_sig m))).
simpl.
	refine (f_equal (fun f => f C) (mds_assoc (proj2_sig m))).
Qed.

Definition alg_join := (exist _ alg_join_set alg_join_prop
	) : alg_md m.

End alg_join.



(** canonical conversion of an adjunction into a monad *)

Section adj2md.
Variable (cats cata:sigT category) (a:adjunction cats cata).

Definition adj2md_set := (Build_md_set
	(adjU a # adjF a) (adj_ret a)
	(adjU a <' adj_fold a '> adjF a)
	) : md_set cats.

Definition adj2md_prop : md_prop adj2md_set.
Proof.
unfold adj2md_set.
destruct a as [adjs adjp].
destruct adjs as [F U ret fold].
unfold adjU, adjsU, adjF, adjsF, adj_ret, adjs_ret, adj_fold, adjs_fold.
simpl.
(*
Check (refl_equal _
	) : ntf ret >$ U >$ F >$ U >$ F >$ U >$ F >$ U
@$ ntf ret >$ U >$ F >$ U >$ F >$ U
	= ntf ret >$ U >$ F >$ U >$ F >$ U >$ F >$ U
@$ ntf ret >$ U >$ F >$ U >$ F >$ U.
Check (refl_equal _
	) : ret '> U '> F '> U '> F '> U '> F '> U @ ret '> U '> F '> U '> F '> U
	= ret '> U '> F '> U '> F '> U '> F '> U @ ret '> U '> F '> U '> F '> U.
*)
refine (Build_md_prop _ _ _ _).
simpl.
	unfold nt_eq_set, ntf.
	simpl.
	change (nt_id_set (U # F) = (U <$ ntf fold @$ ntf ret >$ U) >$ F).
	refine (let p0 := adjs_nt_eq_u adjp in _).
	clearbody p0.
	simpl in p0.
	unfold nt_eq_set, ntf in p0.
	simpl in p0.
	refine (match p0 in _=dep
		return _ = dep >$ _
		with refl_equal => _ end).
	refine (refl_equal _).
simpl.
	unfold nt_eq_set, ntf.
	simpl.
	change (nt_id_set (U # F)
		= U <$ (ntf fold >$ F) @$ U <$ (F <$ ntf ret)).
	refine (match sym_eq (comp_nt_fr_mor_distrib_set _ _ _) in _=dep
		return _ = dep
		with refl_equal => _ end).
	refine (let p0 := adjs_nt_eq_f adjp in _).
	clearbody p0.
	simpl in p0.
	unfold nt_eq_set, ntf in p0.
	simpl in p0.
	refine (match p0 in _=dep
		return _ = _ <$ dep
		with refl_equal => _ end).
	refine (comp_nt_fr_mor_set_id _ _).
simpl.
	unfold nt_eq_set, ntf.
	simpl.
	change ((U <$ ntf fold @$ U <$ ntf fold >$ F >$ U) >$ F
		= (U <$ ntf fold @$ U <$ F <$ U <$ ntf fold) >$ F).
	refine (f_equal (fun a => a >$ F) _).
	change (U <$ ntf fold @$ U <$ (ntf fold >$ F >$ U) =
		U <$ ntf fold @$ U <$ F <$ U <$ ntf fold).
	refine (match sym_eq (comp_nt_fr_mor_distrib_set _ _ _) in _=dep
		return dep = _
		with refl_equal => _ end).
	change (U <$ (ntf fold @$ ntf fold >$ F >$ U) =
		U <$ ntf fold @$ U <$ (F <$ U <$ ntf fold)).
	refine (match sym_eq (comp_nt_fr_mor_distrib_set _ _ _) in _=dep
		return _ = dep
		with refl_equal => _ end).
	refine (f_equal (fun a => U <$ a) _).
	refine (nt_comm fold fold).
Qed.

Definition adj2md := (exist _ adj2md_set adj2md_prop) : md cats.



(** ⟨U C,U ε C⟩ is an algebra over a monad *)

Section alg_fold.
Variable C:projT1 cata.

Definition alg_fold_set := Build_alg_md_set adj2md
	(fr_ob (adjU a) C) (ntf (adjU a <' adj_fold a) C).

Definition alg_fold_prop : alg_md_prop alg_fold_set.
Proof.
refine (Build_alg_md_prop _ _ _ _).
simpl.
	unfold adj2md, md_ret.
	simpl.
	refine (let p := f_equal (fun f => f C)
		(adjs_nt_eq_u (proj2_sig a)) in _).
	clearbody p.
	simpl in p.
	refine (p).
simpl.
	unfold adj2md, md_fr.
	simpl.
	refine (match sym_eq (frs_pres_comp (proj2_sig (adjU a)) _ _)
		in _=dep return dep = _
		with refl_equal => _ end).
	refine (match sym_eq (frs_pres_comp (proj2_sig (adjU a)) _ _)
		in _=dep return _ = dep
		with refl_equal => _ end).
	refine (f_equal (fun m => frs_mor (proj1_sig (adjU a)) m) _).
	refine (let p := f_equal (fun f => f C)
		(nt_comm (adj_fold a) (adj_fold a)) in _).
	clearbody p.
	simpl in p.
	unfold nt_comp_set, comp_nt_fr_mor_set, comp_nt_fr_ob_set
		, fr_id, fr_id_set, fr_mor, fr_ob in p.
	simpl in p.
	refine (p).
Qed.
Eval unfold alg_md in alg_md adj2md.

Definition alg_fold := (exist _ alg_fold_set alg_fold_prop
	) : alg_md adj2md.

End alg_fold.

End adj2md.