From 7529edb3027da350671d9295129ee655d0112d55 Mon Sep 17 00:00:00 2001
From: Philip Kaludercic <philip.kaludercic@fau.de>
Date: Fri, 22 Mar 2024 15:03:40 +0100
Subject: [PATCH] Add Worwell's theorem
---
coalgebra.tex | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/coalgebra.tex b/coalgebra.tex
index c8c9602..0df45f0 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
--
GitLab