Require Import interfaces.Category.
Require Import interfaces.Functor.
Require Import interfaces.Adjunctions.

Module Type MonadDefinition (C : CategoryDefinition).
  Include FunctorDefinition C C.

  Parameter eta : ∀ X, C.m X (omap X).
  Parameter mu : ∀ X, C.m (omap (omap X)) (omap X).

  Axiom eta_natural :
    ∀ {X Y} (f : C.m X Y),
      C.compose (eta Y) f = C.compose (fmap f) (eta X).

  Axiom mu_natural :
    ∀ {X Y} (f : C.m X Y),
      C.compose (mu Y) (fmap (fmap f)) = C.compose (fmap f) (mu X).

  Axiom mu_eta_l :
    ∀ X,
      C.compose (mu X) (eta (omap X)) = C.id (omap X).

  Axiom mu_eta_r :
    ∀ X,
      C.compose (mu X) (fmap (eta X)) = C.id (omap X).

  Axiom mu_mu :
    ∀ X,
      C.compose (mu X) (mu (omap X)) = C.compose (mu X) (fmap (mu X)).

End MonadDefinition.

Module MonadTheory (C : Category) (T : MonadDefinition C).
  Import T.

  Definition ext {X Y} (f : C.m X (T.omap Y)) : C.m (T.omap X) (T.omap Y) :=
    C.compose (mu Y) (fmap f).

  Proposition ext_eta_l X :
    ext (eta X) = C.id (omap X).

  Proposition ext_eta_r {X Y} (f : C.m X (omap Y)) :
    C.compose (ext f) (eta X) = f.

  Proposition ext_ext {X Y Z} (f : C.m X (omap Y)) (g : C.m Y (omap Z)) :
    C.compose (ext g) (ext f) = ext (C.compose (ext g) f).

  Module Kl <: Category.
    Definition t := C.t.
    Definition m X Y := C.m X (T.omap Y).

    Definition id X := eta X.
    Definition compose {X Y Z} (g : m Y Z) (f : m X Y) := C.compose (ext g) f.

    Proposition compose_id_left {X Y} (f : m X Y) :
      compose (id Y) f = f.

    Proposition compose_id_right {X Y} (f : m X Y) :
      compose f (id X) = f.

    Proposition compose_assoc {X Y Z T} (f : m X Y) (g : m Y Z) (h : m Z T) :
      compose (compose h g) f = compose h (compose g f).

    Include CategoryTheory.
  End Kl.

  Module KlF <: Functor C Kl.

    Definition omap (X : C.t) : Kl.t := X.
    Definition fmap {X Y} (f : C.m X Y) : Kl.m X Y := C.compose (eta Y) f.

    Proposition fmap_id X :
      fmap (C.id X) = Kl.id X.

    Proposition fmap_compose {X Y Z} (g : C.m Y Z) (f : C.m X Y) :
      fmap (C.compose g f) = Kl.compose (fmap g) (fmap f).

    Include FunctorTheory C Kl.
  End KlF.

  Module KlU <: Functor Kl C.

    Definition omap (X : Kl.t) : C.t := T.omap X.
    Definition fmap {X Y} (f : Kl.m X Y) : C.m (omap X) (omap Y) := ext f.

    Proposition fmap_id X :
      fmap (Kl.id X) = C.id (omap X).

    Proposition fmap_compose {X Y Z} (g : Kl.m Y Z) (f : Kl.m X Y) :
      fmap (Kl.compose g f) = C.compose (fmap g) (fmap f).

    Include FunctorTheory Kl C.
  End KlU.

  Module KlA <: AdjointFunctors C Kl KlF KlU.

    Definition unit A : C.m A (KlU.omap (KlF.omap A)) :=
      T.eta A.
    Definition counit X : Kl.m (KlF.omap (KlU.omap X)) X :=
      C.id (T.omap X).

    Proposition unit_natural {A V} (f : C.m A V) :
      C.compose (unit V) f = C.compose (KlU.fmap (KlF.fmap f)) (unit A).

    Proposition counit_natural {X Y} (ϕ : Kl.m X Y) :
      Kl.compose (counit Y) (KlF.fmap (KlU.fmap ϕ)) = Kl.compose ϕ (counit X).

    Proposition unit_counit X :
      C.compose (KlU.fmap (counit X)) (unit (KlU.omap X)) = C.id (KlU.omap X).

    Proposition counit_unit A :
      Kl.compose (counit (KlF.omap A)) (KlF.fmap (unit A)) = Kl.id (KlF.omap A).

    Include AdjointFunctorsTheory C Kl KlF KlU.
  End KlA.

End MonadTheory.

Module Type Monad (C : Category) :=
  MonadDefinition C <+
  MonadTheory C.

Require Import ConcreteCategory.

Module ConcreteMonadTheory (C : ConcreteCategory) (T : Monad C).

  Notation "'do' x <- t ;; f" := (C.apply (T.ext (fun x ⇒ f)) t)
    (right associativity, x binder, at level 60).

  Notation ret := (C.apply (T.eta _)).

End ConcreteMonadTheory.

Module Type ConcreteMonad (C : ConcreteCategory) :=
  Monad C <+
  ConcreteMonadTheory C.