diff --git a/coalgebra.tex b/coalgebra.tex index c8c9602a99a379652ad58060d182bba0f05e6642..0df45f0281077edf5d3c3c2d94534c3f85b1419e 100644 --- a/coalgebra.tex +++ b/coalgebra.tex @@ -41,6 +41,13 @@ \[ \nu F = \colim_{n < \omega} F^n \terminal. \] \end{definition} +\begin{theorem}[Worwell] + For a \de{finitary} \de{functor} \(F\), + \(\nu F = F^{\omega+\omega}1\), that is to say one extends and + repeats the \(\op{\omega}\)-chain, starting with + \(\nu F = F^\omega\) instead of \(\terminal\). +\end{theorem} + \begin{definition}\label{def:beheqiv} For a \de{endofunctor} \(F : \map{\Set}{\Set}\) and two \fca{} \((C, c)\), \((D, d)\), are \emph{behaviourally equivalent} for