PS

Initial algebras with parameters

圏論 命題 F-algebra

命題

  • functor: F : \mathcal{D} \to \mathcal{C} ^ \mathcal{C}
  • initial algebraの族: \big( \mathtt{in} _ a : (Fa)( \mu ( Fa ) ) \to \mu ( Fa ) \big) _ { a \in \mathcal{D} }

について

  • F ^ \mu (a) = \mu ( Fa )
  • ( \mathtt{in} _ a ) _ a : \text{natural}

なるfunctor:

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

がただ一つ存在する。

証明

  • F ^ \mu (a \overset{f}{\to} b) := \mathtt{fold} \big( (Fa)(\mu(F b)) \overset{(Ff) _ { \mu(Fb) } }{\to} (Fb)(\mu(Fb)) \overset{\mathtt{in} _ b}{\to} \mu(Fb) \big)

参考文献