Work on coalgebras

thesis/.vscode/ltex.dictionary.en-US.txt

@@ -50,3 +50,5 @@ coproduct
 adjunction
 counit
 epi
+F-coalgebra
+F-coalgebras

thesis/bib.bib

@@ -98,6 +98,13 @@
   keywords   = {premonoidal categories, categories, partiality and partial categories, abstract Kleish, commutative strong monads}
 }
 
+@book{inductive,
+  title     = {Categorical programming with inductive and coinductive types},
+  author    = {Vene, Varmo},
+  year      = {2000},
+  publisher = {Citeseer}
+}
+
 @inproceedings{Lane1971,
   title  = {Categories for the Working Mathematician},
   author = {Saunders Mac Lane},
@@ -123,6 +130,13 @@
   numpages   = {38}
 }
 
+@online{nad-delay,
+  author  = {Nils Anders Danielsson},
+  title   = {The delay monad, defined coinductively},
+  url     = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
+  urldate = {2024-15-02}
+}
+
 @article{param-corec,
   title    = {Parametric corecursion},
   journal  = {Theoretical Computer Science},
@@ -240,10 +254,3 @@
   biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
   bibsource  = {dblp computer science bibliography, https://dblp.org}
 }
-
-@online{nad-delay,
-  author = {Nils Anders Danielsson},
-  title = {The delay monad, defined coinductively},
-  url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
-  urldate = {2024-15-02}
-}

thesis/src/01_preliminaries.tex

@@ -112,8 +112,55 @@ Categories with finite products (i.e. binary products and a terminal object) are
 A cartesian closed category is a cartesian category $\C$ that also has an exponential object $X^Y$ for any $X, Y \in \C$.
 The internal logic of cartesian closed categories is the simply typed $\lambda$-calculus, which makes them a suitable target for interpreting programming languages. For the rest of this thesis we will work in an ambient distributive category that however does not have to be cartesian closed as to be more general.
 
-\section{Coalgebras}
-\todo[inline]{Maybe introduce (co-)induction here via (co-)algebras}
+\section{Functor Coalgebras}
+Let $F : \C \rightarrow \C$ be an endofunctor. Recall that F-algebras are tuples $(X, \alpha : FX \rightarrow X)$ consisting of an object of $\C$ and a morphism out of the functor. Initial F-algebras have been studied extensively as a means of modelling inductive data types together with induction and recursion principles~\cite{inductive}. For this thesis we will be more interested in the dual concept namely terminal coalgebras let us formally introduce them now.
+
+\begin{definition}[F-Coalgebra]
+  A tuple $(X \in \obj{\C}, \alpha : X \rightarrow FX)$ is called a terminal F-coalgebra.
+\end{definition}
+
+\begin{definition}[Morphisms between Coalgebras]\label{def:coalgmorph}
+  Let $(X \in \obj{\C} , \alpha : X \rightarrow FX)$ and $(Y \in \obj{\C} , \beta : Y \rightarrow FY)$ be two F-coalgebras. A morphism between these coalgebras is a morphism $f : X \rightarrow Y$ such that the following diagram commutes:
+  % https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIl0sWzAsMiwiWSJdLFsyLDAsIkZYIl0sWzIsMiwiRlkiXSxbMSwzLCJcXGJldGEiXSxbMCwyLCJcXGFscGhhIl0sWzAsMSwiZiIsMl0sWzIsMywiRmYiXV0=
+  \[\begin{tikzcd}[ampersand replacement=\&]
+    X \&\& FX \\
+    \\
+    Y \&\& FY
+    \arrow["\beta", from=3-1, to=3-3]
+    \arrow["\alpha", from=1-1, to=1-3]
+    \arrow["f"', from=1-1, to=3-1]
+    \arrow["Ff", from=1-3, to=3-3]
+  \end{tikzcd}\]
+  
+\end{definition}
+
+\begin{proposition}
+  F-coalgebras together with their morphisms form a category that we call $Coalg(F)$.
+\end{proposition}
+\begin{proof}
+  Let $(X , \alpha : X \rightarrow FX)$ be an F-coalgebra. The identity morphism on $(X , \alpha)$ is the identity morphism of $\C$ that trivially satisfies $\alpha \circ id = Fid \circ \alpha$.
+
+  Let $(X , \alpha : X \rightarrow FX), (Y, \beta : Y \rightarrow FY)$ and $(Z , \gamma : Z \rightarrow FZ)$ be F-coalgebras.
+  Composition of $f : (X, \alpha) \rightarrow (Y, \beta)$ and $g : (Y, \beta) \rightarrow (Z, \gamma)$ is composition of the underlying morphisms in $\C$ where:
+  \begin{alignat*}{1}
+    &\gamma \circ g \circ f\\
+    =\;&Fg \circ \beta \circ f\\
+    =\;&Fg \circ Ff \circ \alpha\\
+    =\;&F(g \circ f) \circ \alpha 
+  \end{alignat*}
+\end{proof}
+
+The terminal object of $Coalg(F)$ is sometimes called \textit{final F-coalgebra} and can now similarly to initial F-algebras be used for modelling the semantics of coinductive data types. Another special property arises:
+
+\todo[inline]{Characterize final coalgebra first, introduce notation with double bracket}
+
+\begin{theorem}[Lambek's Lemma]
+  Let $(T, t : T \rightarrow FT)$ be a terminal F-coalgebra. Then $t$ is an isomorphism.
+\end{theorem}
+\begin{proof}
+  
+\end{proof}
+
 \todo[inline]{Introduce (terminal) coalgebras, prove Lambek's lemma}
 
 \section{Adjunctions and Free Objects}
@@ -137,6 +184,8 @@ The internal logic of cartesian closed categories is the simply typed $\lambda$-
 
 Free objects are constructions capturing the essence of structures in a minimal way, we will rely on free structures in chapter~\ref{chp:iteration} to define a monad in a general setting. We recall the definition to establish some notation:
 
+\todo[inline]{Change free object notation from llbracket to something else (llbracket is better for terminal coalg)}
+
 \begin{definition}[Free Object]\label{def:free}
 Let $\C, \D$ be categories and $U : \C \rightarrow \D$ be a forgetful functor (whose construction usually is obvious). A free object on some object $X \in \obj{\D}$ is an object $FX \in \obj{\C}$ together with a morphism $\eta : X \rightarrow UFX$ such that the following universal property holds for any $Y \in \obj{\C}$ and $f : X \rightarrow UY$:
 % https://q.uiver.app/#q=WzAsMyxbMCwwLCJYIl0sWzEsMCwiVVkiXSxbMCwxLCJGWCJdLFswLDEsImYiXSxbMCwyLCJcXGV0YSIsMl0sWzIsMSwiXFxleGlzdHMhXFxsbGJyYWNrZXQgZiBcXHJyYnJhY2tldCIsMl1d