PS

Fixed-point functor

命題

Initial algebraの族:

  •  (\mathtt{in} ^ F : F(\mu F) \to \mu F) _ { F \in \mathcal{C} ^ \mathcal{C} }

について

なるfunctor:

  •  \mu : \mathcal{C} ^ \mathcal{C} \to \mathcal{C}

がただ一つ存在する。

証明

  •  \mu ( F \overset{\alpha}{\Rightarrow} G ) := \mathtt{fold} ^ F ( F(\mu G) \overset{\alpha _ {\mu G} }{\to} G(\mu G) \overset{\mathtt{in} _ G}{\to} \mu G )

Fusion law

  •  \mathtt{fold} ^ G (GB \overset{b}{\to} B) \circ \mu(F \overset{\alpha}{\Rightarrow} G) = \mathtt{fold} ^ F (FB \overset{\alpha _B}{\to} GB \overset{b}{\to} B)

vs. Parameterized algebra

参考文献