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)$

参考文献

art08_geuvers_poll.pdf

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