PS

Primitive recursion

(Primitive recursive function圏論による表現) *1

命題

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

について

  •  g \circ T ( \langle h, 1  _ A \rangle) = h \circ i

なる  \mathcal{C}-morphism:

  •  h : A \to B  (paramorphism)

がただ一つ存在する。

証明

  •  h := \pi _ B \circ \mathrm{cata}( \langle g, i \circ T(\pi _ A) \rangle)

参考文献

*1:かえって分かりやすい(と思う)