PS

Kleisli category

Kleisli category

Monad  (T : \mathcal{C} \rightarrow \mathcal{C}, \eta, \mu) について、kleisli category:

  •  \mathcal{C} _ T

を次のように定義できる。

  •  (\mathcal{C} _ T) _ 0 = \mathcal{C} _ 0
  •  (\mathcal{C} _ T) _ 1 = \lbrace f : X \rightarrow T(Y) \mid X, Y \in \mathcal{C} _ 0, f \in \mathcal{C} _ 1 \rbrace
  •  \text{dom}(f: X \rightarrow T(Y)) = X
  •  \text{cod}(f: X \rightarrow T(Y)) = Y
  •  (g : Y \rightarrow T(Z)) \circ (f: X \rightarrow T(Y)) = \mu _ Z \circ T(g) \circ f
  •  \text{id} _ X = \eta _ X

Monadはcategoryだった、ということ。

参考文献