Add Worwell's theorem

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