CategoryTheory/algprog
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Work on initial algebra construction, rework limits

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-30 18:11:52 +01:00
parent 479336a7dd
commit 5bae77ae05
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 261 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
tex/.vscode/ltex.dictionary.en-US.txt vendored
View file

@ -51,3 +51,14 @@ corecursion
bisimulation
bisimilar
bisimilarity
fixpoint
supremum
fixpoints
suprema
CPOs
monotonicity
cocomplete
colimits
colimit
finitary
Finitary

17
tex/catprog.sty
View file

@ -10,6 +10,9 @@
%
% COPIED FROM https://gitlab.cs.fau.de/i8/TexCommon/ AND THEN ADJUSTED.
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{catprog}[2024/03/30 Macros for Category Theory and Semantics]
\RequirePackage{bm} % Needed for defbbname
\RequirePackage{mathtools} % Needed for coloneqq
@ -52,6 +55,7 @@
\providecommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
%% Dual category
\providecommand{\dual}[1]{\ensuremath{#1^{op}}}
\providecommand{\ite}[3]{\oname{if}#1\oname{then}#2\oname{else}}
% Misc
%% Commutation of diagrams
@ -61,7 +65,7 @@
\providecommand{\cata}[1]{\llparenthesis #1 \rrparenthesis}
% Lens brackets for anamorphisms https://unicodeplus.com/U+3016
\providecommand{\ana}[1]{〖 #1 〗}
\providecommand{\dom}{\oname{dom}}
\providecommand{\eps}{{\operatorname\epsilon}}
\providecommand{\amp}{\mathbin{\&}}
@ -222,4 +226,13 @@
% \providecommand{\ift}[3]{\mfix{if}{\mathbin{}#1}{then}{\mathbin{}#2}{else}{\mathbin{}#3}}
% \providecommand{\case}[3]{\mfix{case}{\mathbin{}#1}{of}{#2}{\kern-1pt;}{\mathbin{}#3}}
%%% Overwrite greek letters with var versions https://tex.stackexchange.com/a/304576/292879
\AfterBeginDocument{
\renewcommand{\epsilon}{\varepsilon}
\renewcommand{\theta}{\vartheta}
\renewcommand{\theta}{\vartheta}
\renewcommand{\kappa}{\varkappa}
\renewcommand{\rho}{\varrho}
\renewcommand{\phi}{\varphi}
}
%%%

BIN
tex/main.pdf
View file

Binary file not shown.

119
tex/sections/02_categories.tex
View file

@ -1014,13 +1014,36 @@ Limits are an abstraction of products and many other categorical concepts.
The notion of limit can be instantiated to many interesting notions:
\begin{definition}[Products (as limits)]
Let $\CD$ be the discrete category with 2 elements. Diagrams $D$ are pairs $(A,B)$ of objects of $\CC$, cones are pairs of morphisms
\[A \overset{f}{\longleftarrow} C \overset{g}{\longrightarrow} B\]
and limits of such diagrams are exactly products:
\[A \overset{\fst}{\longleftarrow} A\times B \overset{\snd}{\longrightarrow} B.\]
\begin{definition}[Terminal object (as limit)]
Let $\CD$ be the empty category $\emptyset$.
Diagrams of $\CD$ are empty and thus cones consist of just the apex $C\in\obj{\CC}$.
This also means that every object in $\CC$ forms a cone for this diagram.
The limit $1 \in \obj{\CC}$ is thus the terminal object, since for any $C \in \obj{\CC}$ there is a unique morphism $\bang : C \to 1$.
\end{definition}
\begin{definition}[Product (as limit)]
Let $\CD$ be the discrete category with 2 elements. Diagrams $D$ are pairs $(A,B)$ of objects of $\CC$, cones are pairs of morphisms
% https://q.uiver.app/#q=WzAsMyxbMSwwLCJDIl0sWzAsMSwiQSJdLFsyLDEsIkIiXSxbMCwxLCJmIiwyXSxbMCwyLCJnIl1d
\[\begin{tikzcd}
& C \\
A && B
\arrow["f"', from=1-2, to=2-1]
\arrow["g", from=1-2, to=2-3]
\end{tikzcd}\]
and limits of such diagrams are exactly products:
% https://q.uiver.app/#q=WzAsNCxbMSwyLCJBIFxcdGltZXMgQiJdLFswLDMsIkEiXSxbMiwzLCJCIl0sWzEsMCwiRCJdLFswLDEsIlxcZnN0IiwyXSxbMCwyLCJcXHNuZCJdLFszLDEsImYiLDIseyJjdXJ2ZSI6NH1dLFszLDIsImciLDAseyJjdXJ2ZSI6LTR9XSxbMywwLCJcXGV4aXN0cyFcXGxhbmdsZSBmLGcgXFxyYW5nbGUiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
\[\begin{tikzcd}
& D \\
\\
& {A \times B} \\
A && B
\arrow["\fst"', from=3-2, to=4-1]
\arrow["\snd", from=3-2, to=4-3]
\arrow["f"', curve={height=24pt}, from=1-2, to=4-1]
\arrow["g", curve={height=-24pt}, from=1-2, to=4-3]
\arrow["{\exists!\langle f,g \rangle}", dashed, from=1-2, to=3-2]
\end{tikzcd}\]\end{definition}
\begin{definition}[Equalizer]
Let $\CD$ be a category with two non-trivial and parallel morphisms $u,v : 1 \to 2$. Diagrams are parallel morphisms
% https://q.uiver.app/#q=WzAsMixbMCwwLCJBXzEiXSxbMiwwLCJBXzIiXSxbMCwxLCJmIiwwLHsib2Zmc2V0IjotMX1dLFswLDEsImciLDIseyJvZmZzZXQiOjF9XV0=
@ -1029,30 +1052,34 @@ The notion of limit can be instantiated to many interesting notions:
\arrow["f", shift left, from=1-1, to=1-3]
\arrow["g"', shift right, from=1-1, to=1-3]
\end{tikzcd}\]
and cones are pairs of morphisms $c : C \to A_1, d C \to A_2$, such that $f \comp c = d = g \comp c$:
% https://q.uiver.app/#q=WzAsMyxbMCwyLCJBXzEiXSxbMiwyLCJBXzIiXSxbMCwwLCJDIl0sWzAsMSwiZiIsMCx7Im9mZnNldCI6LTF9XSxbMCwxLCJnIiwyLHsib2Zmc2V0IjoxfV0sWzIsMCwiYyIsMl0sWzIsMSwiZCJdXQ==
and cones are pairs of morphisms $c : C \to A_1, d : C \to A_2$, such that $f \comp c = d = g \comp c$:
% https://q.uiver.app/#q=WzAsMyxbMCwyLCJBXzEiXSxbMiwyLCJBXzIiXSxbMSwwLCJDIl0sWzAsMSwiZiIsMCx7Im9mZnNldCI6LTF9XSxbMCwxLCJnIiwyLHsib2Zmc2V0IjoxfV0sWzIsMCwiYyIsMl0sWzIsMSwiZCJdXQ==
\[\begin{tikzcd}
C \\
& C \\
\\
{A_1} && {A_2}
\arrow["f", shift left, from=3-1, to=3-3]
\arrow["g"', shift right, from=3-1, to=3-3]
\arrow["c"', from=1-1, to=3-1]
\arrow["d", from=1-1, to=3-3]
\arrow["c"', from=1-2, to=3-1]
\arrow["d", from=1-2, to=3-3]
\end{tikzcd}\]
A limit of such a diagram is called an \emph{equalizer} of $f$ and $g$:
% https://q.uiver.app/#q=WzAsNCxbMiwyLCJBXzEiXSxbNCwyLCJBXzIiXSxbMiwwLCJDIl0sWzAsMiwiRSJdLFswLDEsImYiLDAseyJvZmZzZXQiOi0xfV0sWzAsMSwiZyIsMix7Im9mZnNldCI6MX1dLFsyLDAsIlxcZm9yYWxsIGMiLDJdLFsyLDEsImQiXSxbMywwLCJlIl0sWzIsMywiXFxleGlzdHMhaCIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
% https://q.uiver.app/#q=WzAsNCxbMCw0LCJBXzEiXSxbMiw0LCJBXzIiXSxbMSwyLCJFIl0sWzEsMCwiQyJdLFswLDEsImYiLDAseyJvZmZzZXQiOi0xfV0sWzAsMSwiZyIsMix7Im9mZnNldCI6MX1dLFsyLDAsImUiLDJdLFsyLDFdLFszLDIsIlxcZXhpc3RzISBoIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzMsMCwiYyIsMix7ImN1cnZlIjozfV0sWzMsMSwiIiwwLHsiY3VydmUiOi0zfV1d
\[\begin{tikzcd}
&& C \\
& C \\
\\
E && {A_1} && {A_2}
\arrow["f", shift left, from=3-3, to=3-5]
\arrow["g"', shift right, from=3-3, to=3-5]
\arrow["{\forall c}"', from=1-3, to=3-3]
\arrow["d", from=1-3, to=3-5]
\arrow["e", from=3-1, to=3-3]
\arrow["{\exists!h}"', dashed, from=1-3, to=3-1]
& E \\
\\
{A_1} && {A_2}
\arrow["f", shift left, from=5-1, to=5-3]
\arrow["g"', shift right, from=5-1, to=5-3]
\arrow["e"', from=3-2, to=5-1]
\arrow[from=3-2, to=5-3]
\arrow["{\exists! h}"', dashed, from=1-2, to=3-2]
\arrow["c"', curve={height=18pt}, from=1-2, to=5-1]
\arrow[curve={height=-18pt}, from=1-2, to=5-3]
\end{tikzcd}\]
where the unnamed morphisms are usually omitted.
\end{definition}
% TODO equalizer in Set
@ -1079,7 +1106,50 @@ The notion of limit can be instantiated to many interesting notions:
\end{proof}
\begin{definition}[Pullback]
% TODO pullback
Let $\CD$ be a poset category illustrated by the following diagram:
% https://q.uiver.app/#q=WzAsMyxbMSwwLCJcXGJ1bGxldCJdLFswLDEsIlxcYnVsbGV0Il0sWzIsMSwiXFxidWxsZXQiXSxbMCwxXSxbMCwyXV0=
\[\begin{tikzcd}
& \bullet \\
\bullet && \bullet
\arrow[from=1-2, to=2-1]
\arrow[from=1-2, to=2-3]
\end{tikzcd}\]
Diagrams consist of two arrows with the same codomain.
Cones are of the form:
% https://q.uiver.app/#q=WzAsNixbMiwwLCJDIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJEIl0sWzEsMiwiXFxjb21tIl0sWzMsMiwiXFxjb21tIl0sWzAsMSwiZiIsMl0sWzAsMiwiZyJdLFsxLDMsIm0iLDJdLFsyLDMsIm4iXSxbMCwzLCJoIiwyXV0=
\[\begin{tikzcd}
&& C \\
\\
A & \comm && \comm & B \\
\\
&& D
\arrow["f"', from=1-3, to=3-1]
\arrow["g", from=1-3, to=3-5]
\arrow["m"', from=3-1, to=5-3]
\arrow["n", from=3-5, to=5-3]
\arrow["h"', from=1-3, to=5-3]
\end{tikzcd}\]
where $h$ is usually omitted, and instead the condition is expressed as $m\comp f = n \comp g$.
Limits of such diagrams are called \emph{pullbacks} usually denoted in the following way:
% https://q.uiver.app/#q=WzAsNSxbMiwyLCJQIl0sWzAsNCwiQSJdLFs0LDQsIkIiXSxbMiw2LCJEIl0sWzIsMCwiQyJdLFswLDEsInBfMSIsMl0sWzAsMiwicF8yIl0sWzEsMywiZiIsMl0sWzIsMywiZyJdLFs0LDEsImEiLDIseyJjdXJ2ZSI6M31dLFs0LDIsImIiLDAseyJjdXJ2ZSI6LTN9XSxbNCwwLCJcXGV4aXN0cyEgaCIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFswLDMsIiIsMix7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ==
\[\begin{tikzcd}
&& C \\
\\
&& P \\
\\
A &&&& B \\
\\
&& D
\arrow["{p_1}"', from=3-3, to=5-1]
\arrow["{p_2}", from=3-3, to=5-5]
\arrow["f"', from=5-1, to=7-3]
\arrow["g", from=5-5, to=7-3]
\arrow["a"', curve={height=18pt}, from=1-3, to=5-1]
\arrow["b", curve={height=-18pt}, from=1-3, to=5-5]
\arrow["{\exists! h}"', dashed, from=1-3, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=3-3, to=7-3]
\end{tikzcd}\]
\end{definition}
% TODO pullback in Set
% \begin{example}
@ -1089,6 +1159,9 @@ The notion of limit can be instantiated to many interesting notions:
\begin{proposition}
Limits are unique up to isomorphism.
\end{proposition}
\begin{proof}
% TODO proof that limits are up to iso
\end{proof}
\begin{definition}[Complete Category]
A category $\CC$ is called \emph{complete} if every diagram in $\CC$ has a limit.
@ -1097,6 +1170,9 @@ The notion of limit can be instantiated to many interesting notions:
\begin{proposition}
$\CC$ is complete iff $\CC$ has all products and equalizers, i.e.\ using products and equalizer one can construct arbitrary limits.
\end{proposition}
\begin{proof}
% TODO proof that complete iff products and eq
\end{proof}
\begin{definition}[Finitely Complete Category]
A category $\CC$ is called \emph{finitely complete} if every finite diagram in $\CC$ has a limit.
@ -1111,6 +1187,9 @@ The notion of limit can be instantiated to many interesting notions:
\item $\CC$ has a terminal object and pullbacks
\end{enumerate}
\end{proposition}
\begin{proof}
% TODO proof of finitely complete criterions
\end{proof}
\section{Colimits}

136
tex/sections/03_constructions.tex
View file

@ -1,4 +1,140 @@
\chapter{Constructions}
\section{CPO}
Recall that $FI \iso I$ for the initial F-algebra $I$, our goal is to construct initial F-algebras as least fixpoints.
Consider for example the faculty function which is defined by the recursive equation
\[fac\;n := \mathrm{if}\; n=0\; \mathrm{then}\; 1 \;\mathrm{else}\; n \cdot fac(n-1).\]
$fac : \mathbb{N} \to \mathbb{N}$ is the \emph{solution} of the previous equation or equivalently the fixpoint of the function $\varphi : \Par(\mathbb{N},\mathbb{N}) \to \Par(\mathbb{N},\mathbb{N})$ defined by
\[\varphi\;f\;n := \mathrm{if}\; n=0\; \mathrm{then}\; 1 \;\mathrm{else}\; n \cdot f(n-1).\]
Thus, $fac$ should satisfy $fac = \varphi(fac)$, which is obtained by iteration of $\varphi$:
\begin{center}
\begin{tabular}{l l l l l}
& 0 & 1 & 2 & \ldots \\\midrule
$\bot$ & & & & \\
$\varphi(\bot)$ & 1 & & & \\
$\varphi(\varphi(\bot))$ & 1 & 1 & & \\
$\varphi(\varphi(\varphi(\bot)))$ & 1 & 1 & 2 & \\
$\ldots$ & & & &
\end{tabular}
\end{center}
Since $\Par(\mathbb{N},\mathbb{N})$ admits a poset structure where $f \sqsubseteq g$ iff $\dom f \subseteq \dom g$ and $\forall x \in \dom f. fx = gx$, we can view $fac$ as the supremum of the ascending chain
\[\bot \sqsubseteq \phi(\bot) \sqsubseteq \phi(\phi(\bot)) \sqsubseteq \ldots.\]
\begin{definition}[Complete Partial Order]
A \emph{complete partial order} (\emph{CPO}) is a poset $(X, \sqsubseteq)$ with
\begin{enumerate}
\item the smallest element $\bot$,
\item suprema for infinite chains:
\[x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq \ldots.\]
\end{enumerate}
We denote the supremum of such chains as $\bigsqcup_i x_i$.
\end{definition}
\begin{example} Examples of CPOs include:
\begin{enumerate}
\item Every set $X$ yields a CPO $(\PSet X, \subseteq)$, where the smallest element is $\emptyset$ and the supremum of chains is the big union.
\item For any $X,Y$ we get a CPO $(\Par(X,Y), \sqsubseteq)$, defined as above. The supremum of a chain $(f_i)$ is defined by
\[ \dom (\bigsqcup_i f_i) = \bigcup_i \dom f_i; \qquad (\bigsqcup_i f_i)(x) = f_i(x), \text{ for a suitable (big enough) } i. \]
\item Every set $X$ yields a CPO $(X_\bot, \sqsubseteq)$, where $X_\bot = X \cup \{ \bot \}$ and $x \sqsubseteq y$ iff $x=y$ or $x = \bot$. This is called the \emph{flat CPO}.
\end{enumerate}
\end{example}
\begin{definition}[Continuous Function]
A function $\phi : (X, \sqsubseteq) \to (X', \sqsubseteq')$ is called \emph{continuous} if
\begin{itemize}
\item $\phi$ is monotonous, i.e.\ $x \sqsubseteq y \Rightarrow \phi(x) \sqsubseteq' \phi(y)$,
\item $\phi$ preserves suprema of chains, i.e.\ $\phi(\bigsqcup x_i) = \bigsqcup' \phi(x_i)$.
\end{itemize}
\end{definition}
\begin{example}
The aforementioned $\phi : \Par(\mathbb{N}, \mathbb{N})$ with $\phi\;f\;n = \ite{n=0}{1}{n \cdot f(n-1)}$ is continuous.
% TODO proof
\end{example}
\begin{theorem}[Kleene's Fixpoint Theorem]
Let $(X, \sqsubseteq)$ be a CPO and let $\phi : X \to X$ be continuous.
The least fixpoint of $\phi$ is
\[\mu\phi = \bigsqcup_i\phi^i(\bot).\]
\end{theorem}
\begin{proof}
$\mu\phi$ is a fixpoint, since
\[\phi(\mu\phi) = \phi (\bigsqcup_i \phi^i(\bot)) = \bigsqcup_i \phi^{i+1}(\bot) = \bigsqcup_i \phi^i(\bot) = \mu\phi.\]
To show that it is the least fixpoint, consider another fixpoint $\phi(x) = x$. To show that $\mu\phi \sqsubseteq x$ it suffices to show that $\phi^i(\bot) \sqsubseteq x$ for all $i \in \mathbb{N}$, which indeed follows by induction:
\begin{mycase}
\case{} $i=0$
\[\
\phi^0(\bot) = \bot \sqsubseteq x\]
\case{} $i = n+1$\\
The induction hypothesis $\phi^n \sqsubseteq x$ directly implies \[\phi^{n+1}(\bot) \sqsubseteq \phi(x) = x\] by monotonicity of $\phi$.
\end{mycase}
\end{proof}
In the next section we will generalize this result categorically to obtain a construction for initial F-algebras.
\section{Initial Algebra Construction}
Consider a cocomplete category $\CC$, $\CC$ has similarities to a CPO, since it has
\begin{itemize}
\item an initial object $0 \overset{\cobang_A}{\longrightarrow} A$,
\item colimits of every $\omega$-chain of morphisms (i.e.\ diagrams $D : (\mathbb{N}, \leq) \to \CC$):
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJBXzAiXSxbMiwwLCJBXzEiXSxbNCwwLCJBXzIiXSxbNiwwLCJcXGxkb3RzIl0sWzIsMiwiQyJdLFswLDQsIlxcaW90YV8wIiwyLHsiY3VydmUiOjJ9XSxbMSw0LCJcXGlvdGFfMSJdLFsyLDQsIlxcaW90YV8yIiwwLHsiY3VydmUiOi0yfV0sWzMsNCwiXFxsZG90cyIsMCx7ImN1cnZlIjotM31dLFswLDEsImFfezAsMX0iXSxbMSwyLCJhX3sxLDJ9Il0sWzIsMywiXFxsZG90cyJdXQ==
\[\begin{tikzcd}
{A_0} && {A_1} && {A_2} && \ldots \\
\\
&& C
\arrow["{\iota_0}"', curve={height=12pt}, from=1-1, to=3-3]
\arrow["{\iota_1}", from=1-3, to=3-3]
\arrow["{\iota_2}", curve={height=-12pt}, from=1-5, to=3-3]
\arrow["\ldots", curve={height=-18pt}, from=1-7, to=3-3]
\arrow["{a_{0,1}}", from=1-1, to=1-3]
\arrow["{a_{1,2}}", from=1-3, to=1-5]
\arrow["\ldots", from=1-5, to=1-7]
\end{tikzcd}\]
\end{itemize}
\begin{definition}[$\omega$-cocontinuity]
A functor $F : \CC \to \CC$ is called \emph{$\omega$-cocontinuous} if $F$ preserves colimits of $\omega$-chains, i.e.\ if for every diagram $D: (\mathbb{N},\leq) \to \CC$:
\[F(\oname{colim} D) \iso \oname{colim}(FD).\]
More concretely, if for every colimit $(C, \iota)$ of $D$, the cone $(FC, F\iota)$ is the colimit of $FD$.
\end{definition}
\begin{definition}[Finitary Functor]
A functor $F : \Set \to \Set$ is called \emph{finitary} if for every $X$ and $x \in FX$ there exists a finite surjective map $m : Y \to X$ and $y \in FY$ such that $x = F\;m\;y$.
\end{definition}
\begin{theorem}
Finitary functors are $\omega$-cocontinuous.
\end{theorem}
\begin{lemma}\label{lem:finclosed}
Finitary functors are closed under
\begin{enumerate}
\item finite products,
\item coproducts,
\item and composition.
\end{enumerate}
\end{lemma}
A consequence of \autoref{lem:finclosed} is that for any signature $\Sigma$, the functor
\[F_\Sigma X = \coprod_{\sigma \in \Sigma} X^{ar(\sigma)}\]
is finitary.
\begin{theorem}
Let $\CC$ be cocomplete and $F : \CC \to \CC$ $\sigma$-cocontinuous. Then $F$ has the initial algebra $I = \oname{colim}_{n\in\mathbb{N}} F^n 0$.
More concretely $I$ is the colimit of the $\omega$-chain:
% https://q.uiver.app/#q=WzAsNSxbMCwwLCIwIl0sWzIsMCwiRjAiXSxbNCwwLCJGRjAiXSxbNiwwLCJcXGxkb3RzIl0sWzIsMiwiXFxtdSBGIl0sWzAsMSwiaSJdLFsxLDIsIkZpIl0sWzIsMywiXFxsZG90cyJdLFswLDQsIlxcaW90YV8wIiwyLHsiY3VydmUiOjJ9XSxbMSw0LCJcXGlvdGFfMSIsMl0sWzIsNCwiXFxpb3RhXzIiLDIseyJjdXJ2ZSI6LTN9XSxbMyw0LCJcXGxkb3RzIiwwLHsiY3VydmUiOi0zfV1d
\[\begin{tikzcd}
0 && F0 && FF0 && \ldots \\
\\
&& {I}
\arrow["i", from=1-1, to=1-3]
\arrow["Fi", from=1-3, to=1-5]
\arrow["\ldots", from=1-5, to=1-7]
\arrow["{\iota_0}"', curve={height=12pt}, from=1-1, to=3-3]
\arrow["{\iota_1}"', from=1-3, to=3-3]
\arrow["{\iota_2}"', curve={height=-18pt}, from=1-5, to=3-3]
\arrow["\ldots", curve={height=-18pt}, from=1-7, to=3-3]
\end{tikzcd}\]
\end{theorem}
\section{Terminal Coalgebra Construction}