import Mathlib.CategoryTheory.Monad.Kleisli
import Mathlib.CategoryTheory.Monad.Algebra
import FormalLab.CategoryTheory.Adjunctions

/-!
# 第53章：モナド・余モナド・Kleisli圏・Eilenberg–Moore圏

ある計算を一段行うと `T(X)` が得られ、さらに同じ計算を重ねると `T(T(X))` が得られるとします。二重の
構造を一段へ平坦化する操作があり、何もしない値を構造へ入れる操作もあれば、反復を一貫して合成できます。
自己関手とこの二つの自然変換をまとめたものがモナドです。

モナドはプログラムの特定の構文ではなく、任意の圏上で定義される構造です。本章では単位、乗法、三法則を
Option型の計算と照合し、Kleisli圏とEilenberg–Moore圏が同じモナドを二方向から組織することを学びます。
射を反転して得られる余モナドも、状態の観察や文脈の複製を表す双対構造として区別します。

## モナドは自己関手上の単位と乗法である

圏 `C` 上のモナド `T` は自己関手 `T:C→C`、自然変換

$$
\eta:\mathrm{Id}_{\mathcal C}\Rightarrow T,
\qquad
\mu:T\mathbin{\circ}T\Rightarrow T
$$

と、結合律および二つの単位律から成ります。

$$
T\mu\mathbin{;}\mu=\mu_T\mathbin{;}\mu,
\qquad
\eta_T\mathbin{;}\mu=\mathrm{id}_T,
\qquad
T\eta\mathbin{;}\mu=\mathrm{id}_T.
$$

`η` は値を一段の構造へ入れ、`μ` は二重の構造を一段へ平坦化します。
-/

namespace FormalLab.CategoryFoundations.Monads

open _root_.CategoryTheory

universe v u

variable {C : Type u} [Category.{v} C]
variable (T : Monad C)

example : C ⥤ C := T.toFunctor
example : 𝟭 C ⟶ (T : C ⥤ C) := T.η
example : (T : C ⥤ C) ⋙ (T : C ⥤ C) ⟶ (T : C ⥤ C) := T.μ

example (X : C) :
    T.map (T.μ.app X) ≫ T.μ.app X = T.μ.app (T.obj X) ≫ T.μ.app X := T.assoc X

example (X : C) : T.η.app (T.obj X) ≫ T.μ.app X = 𝟙 (T.obj X) := T.left_unit X
example (X : C) : T.map (T.η.app X) ≫ T.μ.app X = 𝟙 (T.obj X) := T.right_unit X

/-!
結合律は三重の構造 `T³X` を二通りに平坦化しても同じになることを述べます。左右単位律は、外側または
内側へ自明な一段を加えてから平坦化しても元へ戻ることを述べます。自然性により、これらの操作は `C` の射と
両立します。

恒等関手は、単位と乗法を恒等自然変換とする恒等モナドです。
-/

example : Monad C := Monad.id C

/-!
## Optionで三法則を計算する

型 `Option α` は失敗し得る値を表します。`some` が単位、入れ子になったOptionを一段にする操作が乗法です。
ここでは圏論的な型の圏を構成し直す前に、各型で現れる三法則をLeanの関数として検査します。
-/

def optionUnit {α : Type} (x : α) : Option α := some x

def optionJoin {α : Type} : Option (Option α) → Option α
  | none => none
  | some x => x

theorem optionLeftUnit {α : Type} (x : Option α) :
    optionJoin (optionUnit x) = x := rfl

theorem optionRightUnit {α : Type} (x : Option α) :
    optionJoin (Option.map optionUnit x) = x := by
  cases x <;> rfl

theorem optionAssociative {α : Type} (x : Option (Option (Option α))) :
    optionJoin (Option.map optionJoin x) = optionJoin (optionJoin x) := by
  cases x with
  | none => rfl
  | some y => cases y <;> rfl

theorem optionJoin_nested_value :
    optionJoin (some (some 4) : Option (Option Nat)) = some 4 := rfl

theorem optionJoin_nested_failure :
    optionJoin (some none : Option (Option Nat)) = none := rfl

#eval optionJoin (some (some 4))
#eval optionJoin (some none : Option (Option Nat))

/-!
三定理は `η_T;μ=id`, `Tη;μ=id`, `Tμ;μ=μ_T;μ` の成分計算です。ただし、これだけではOptionが圏論的な
モナドである完全な証明にはなりません。`Option.map` が関手であること、`optionUnit` と `optionJoin` が全関数に
対して自然であることも必要です。対象ごとの法則と自然変換の法則を分けます。

## Kleisli圏は効果を持つ射を合成する

モナド `T` のKleisli圏は `C` と同じ対象を持ち、`X` から `Y` への射を元の圏の射

$$
X\longrightarrow T(Y)
$$

として定めます。`f:X→T(Y)` と `g:Y→T(Z)` の合成は

$$
X\xrightarrow{f}T(Y)\xrightarrow{T(g)}T^2(Z)
  \xrightarrow{\mu_Z}T(Z).
$$

です。恒等射は `η_X:X→T(X)` です。
-/

example (X : C) : Kleisli T := Kleisli.mk T X

example {X Y : C} (f : X ⟶ T.obj Y) :
    Kleisli.Hom (Kleisli.mk T X) (Kleisli.mk T Y) := ⟨f⟩

/-!
OptionモナドではKleisli射は失敗し得る関数です。合成は最初の失敗を保持し、成功した値だけを次の関数へ渡します。
結合律はモナドの結合律、単位律はモナドの二単位律から従います。

## Eilenberg–Moore代数は構造を解釈する

モナド `T` のEilenberg–Moore代数は対象 `A` と作用

$$
a:T(A)\longrightarrow A
$$

を持ち、単位を消去し、二重構造の解釈が一段ずつの解釈と一致することを要求します。

$$
\eta_A\mathbin{;}a=\mathrm{id}_A,
\qquad
\mu_A\mathbin{;}a=T(a)\mathbin{;}a.
$$
-/

variable (A : T.Algebra)

example : C := A.A
example : T.obj A.A ⟶ A.A := A.a
example : T.η.app A.A ≫ A.a = 𝟙 A.A := A.unit
example : T.μ.app A.A ≫ A.a = T.map A.a ≫ A.a := A.assoc

/-!
Optionモナドの代数では、失敗 `none` をどの値として解釈するかを選ぶことに相当します。Kleisli圏が効果を持つ
計算の射を前面に出すのに対し、Eilenberg–Moore圏は効果の結果を一貫して解釈できる対象を集めます。同じ圏では
なく、同じモナドから生じる二つの標準的な圏です。

## 余モナドは全射を反転する

余モナド `G` は自己関手と

$$
\varepsilon:G\Rightarrow\mathrm{Id}_{\mathcal C},
\qquad
\delta:G\Rightarrow G\mathbin{\circ}G
$$

を持ち、余結合律と二つの余単位律を満たします。`ε` は一つの観察を取り出し、`δ` は文脈付きの対象をさらに
文脈付きとして展開します。モナドの `η,μ` の矢印を反転した双対ですが、同じ計算効果の別表記ではありません。
-/

variable (G : Comonad C)

example : (G : C ⥤ C) ⟶ 𝟭 C := G.ε
example : (G : C ⥤ C) ⟶ (G : C ⥤ C) ⋙ G := G.δ
example (X : C) : G.δ.app X ≫ G.ε.app (G.obj X) = 𝟙 (G.obj X) := G.left_counit X

/-!
## 随伴からモナドが生まれる

随伴 `F⊣G` では合成 `F;G:C→C` に単位 `η:Id→FG` があり、余単位を中央で使うと
`FGFG→FG` を得ます。これがモナドの乗法です。逆側の `G;F:D→D` には余モナドが生じます。

しかしモナドの定義自体は随伴をデータとして要求しません。逆に任意のモナドからKleisli随伴と
Eilenberg–Moore随伴を構成できます。次のモナド性の章では、与えられた随伴の右随伴側が
Eilenberg–Moore圏をどこまで回収するかを扱います。

## 要点

* モナドは自己関手、単位 `η`, 乗法 `μ`, 結合律、二つの単位律から成る。
* 対象ごとの平坦化法則に加え、単位と乗法が自然変換であることが必要である。
* Kleisli圏の射 `X→Y` は元の圏の射 `X→T(Y)` で、乗法を使って合成する。
* Eilenberg–Moore代数は作用 `T(A)→A` によってモナド構造を一貫して解釈する。
* 余モナドは余単位と余乗法を持つ双対構造であり、随伴はモナドと余モナドを生む。

## 研究史と文献案内

初期文献では現在のモナドは “triple” や “standard construction” と呼ばれました。Kleisli [KLE65] と
Eilenberg–Moore [EM65] は、随伴から生じるこの構造と二つの標準的な圏を研究した一次資料です。現在の
“monad” という語とモノイド対象としての整理を初期論文へ遡及的に投影しません。現代的定式化は [MAC98]、
Leanの `Monad`, `Kleisli`, `Monad.Algebra` は [MATHLIB] を参照してください。

## 問題

### Optionの自然性まで証明する

任意の関数 `f:α→β` に対し、`Option.map f ∘ optionUnit = optionUnit ∘ f` と、`optionJoin` が二重の
`Option.map` と可換する式を証明してください。各Optionを場合分けし、単位・乗法が対象ごとの関数だけでなく
自然変換をなすことを示します。三つのモナド法則と合わせて、どの証明が自然性でどれが代数法則かを分類できれば
完了です。

### Kleisli合成の圏法則を導く

Kleisli射 `f:X→TY`, `g:Y→TZ`, `h:Z→TW` の合成を `f;Tg;μ` として二段階で展開してください。結合律を
関手法則、`μ` の自然性、モナド結合律へ順に還元します。左右の恒等射 `η` についても二単位律を使い分け、
Kleisli圏の三法則がモナドのどの法則を必要とするか対応表にできれば完了です。

### 二つの標準圏を比較する

同じモナドからKleisli圏とEilenberg–Moore圏の対象・射・合成をそれぞれ書き出してください。Optionモナドを
例に、失敗し得る関数と、失敗を既定値へ解釈する代数を構成します。両者が同じ対象集合を持つ、または同じ圏で
あるとは限らないことを示し、それぞれから元のモナドを生む随伴の向きを説明できれば完了です。
-/

end FormalLab.CategoryFoundations.Monads