PS

fold/build fusion

命題

  • endofunctor:  F : \mathcal{C} \to \mathcal{C}
  • forgetful functor:  U: \operatorname{\mathit{F}-\mathcal{Alg}} \to \mathcal{C}

について、initial algebra:

  •  \mathtt{in} : F(\mu F) \to \mu F

が存在するならば、そのcatamorphimの族:

  •  \big( \mathtt{fold}(h) : \mu F \to U(h) \big) _  { h \in \operatorname{\mathit{F}-\mathcal{Alg}} }

は、mediatorを

  •  \mathtt{build}(\sigma : \Delta C \Rightarrow U) := \sigma _ { \mathtt{in} } : C \to \mu F

とする limiting cone of  U になる:

  •  \mathtt{fold}(h) \circ \mathtt{build}(\sigma) = \sigma _ h  (fold/build fusion)

参考文献