diff --git a/tex/.vscode/ltex.dictionary.en-US.txt b/tex/.vscode/ltex.dictionary.en-US.txt index 785c4eb..f3b49f7 100644 --- a/tex/.vscode/ltex.dictionary.en-US.txt +++ b/tex/.vscode/ltex.dictionary.en-US.txt @@ -51,3 +51,14 @@ corecursion bisimulation bisimilar bisimilarity +fixpoint +supremum +fixpoints +suprema +CPOs +monotonicity +cocomplete +colimits +colimit +finitary +Finitary diff --git a/tex/catprog.sty b/tex/catprog.sty index 8be2316..814c63a 100644 --- a/tex/catprog.sty +++ b/tex/catprog.sty @@ -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} +} +%%% \ No newline at end of file diff --git a/tex/main.pdf b/tex/main.pdf index 14344e8..0903fdb 100644 Binary files a/tex/main.pdf and b/tex/main.pdf differ diff --git a/tex/sections/02_categories.tex b/tex/sections/02_categories.tex index a4aa6ff..4952928 100644 --- a/tex/sections/02_categories.tex +++ b/tex/sections/02_categories.tex @@ -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} diff --git a/tex/sections/03_constructions.tex b/tex/sections/03_constructions.tex index ddf04f5..02c049f 100644 --- a/tex/sections/03_constructions.tex +++ b/tex/sections/03_constructions.tex @@ -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} \ No newline at end of file