PS

Pattern matching

Endofunctor:

  •  T : \mathcal{C} \to \mathcal{C}

について・・・

Lambek's lemma

Every initial algebra is an isomorphism:

  • initial algebra:  i: T(A) \to A
  •  \mathcal{C}-morphism:  g : T(A) \to B *2

について

  •  h \circ i = g

なる  \mathcal{C}-morphism:

  •  h : A \to B

がただ一つ存在する。

参考文献

*1: Afixed pointになっている

*2:いわゆるcase式