somewhat finish coalgebras

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

@@ -48,3 +48,6 @@ coalgebras
 F-coalgebras
 coalgebra
 corecursion
+bisimulation
+bisimilar
+bisimilarity

tex/.vscode/settings.json

@@ -30,5 +30,8 @@
     "\\setmintedinline[]{}": "ignore",
     "\\setmathfont[]{}": "ignore",
     "\\setmathfont{}": "ignore"
+  },
+  "ltex.latex.environments": {
+    "cases": "ignore"
   }
 }

tex/catprog.sty

@@ -146,16 +146,16 @@
 \providecommand{\bigmeet}{\bigsqcap}
 
 %% Products
-\providecommand{\fst}{\oname{fst}}
+\providecommand{\fst}{\pi_1}
-\providecommand{\snd}{\oname{snd}}
+\providecommand{\snd}{\pi_2}
 \providecommand{\pr}{\oname{pr}}
 
 \providecommand{\brks}[1]{\langle #1\rangle}
 \providecommand{\Brks}[1]{\bigl\langle #1\bigr\rangle}
 
 %% Coproducts
-\providecommand{\inl}{\oname{inl}}
+\providecommand{\inl}{\oname{i}_1}
-\providecommand{\inr}{\oname{inr}}
+\providecommand{\inr}{\oname{i}_2}
 \providecommand{\inj}{\oname{in}}
 
 \DeclareSymbolFont{Symbols}{OMS}{cmsy}{m}{n}

tex/sections/02_categories.tex

@@ -164,15 +164,15 @@ This yields a proof principle ``by duality'', where every theorem yields another
 \section{Products and Coproducts}
 The categorical abstraction of Cartesian products is:
 \begin{definition}[Product]
-  The \emph{product} of two objects $A, B \in \obj{\CC}$ is an object that we call $A \times B$ together with morphisms $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$ (the projections), where the following property holds:
+  The \emph{product} of two objects $A, B \in \obj{\CC}$ is an object that we call $A \times B$ together with morphisms $\fst : A \times B \to A$ and $\snd : A \times B \to B$ (the projections), where the following property holds:
   % https://q.uiver.app/#q=WzAsNCxbMiwyLCJBIFxcdGltZXMgQiJdLFs0LDIsIkIiXSxbMCwyLCJBIl0sWzIsMCwiQyJdLFswLDIsIlxccGlfMSJdLFswLDEsIlxccGlfMiIsMl0sWzMsMiwiZiIsMl0sWzMsMSwiZyJdLFszLDAsIlxcZXhpc3RzIVxcbGFuZ2xlIGYsIGcgXFxyYW5nbGUiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
   \[
     \begin{tikzcd}
       && C \\
       \\
       A && {A \times B} && B
-      \arrow["{\pi_1}", from=3-3, to=3-1]
+      \arrow["{\fst}", from=3-3, to=3-1]
-      \arrow["{\pi_2}"', from=3-3, to=3-5]
+      \arrow["{\snd}"', from=3-3, to=3-5]
       \arrow["f"', from=1-3, to=3-1]
       \arrow["g", from=1-3, to=3-5]
       \arrow["{\exists!\langle f, g \rangle}", dashed, from=1-3, to=3-3]
@@ -189,15 +189,15 @@ The categorical abstraction of Cartesian products is:
 \end{example}
 Dual to products are:
 \begin{definition}[Coproduct]
-  The \emph{coproduct} of two objects $A, B \in \obj{\CC}$ is an object that we call $A + B$ together with morphisms $i_1 : A \to A + B$ and $i_2 : B \to A + B$ (the injections), where the following property holds:
+  The \emph{coproduct} of two objects $A, B \in \obj{\CC}$ is an object that we call $A + B$ together with morphisms $\inl : A \to A + B$ and $\inr : B \to A + B$ (the injections), where the following property holds:
   % https://q.uiver.app/#q=WzAsNCxbMiwwLCJBK0IiXSxbMCwwLCJBIl0sWzQsMCwiQiJdLFsyLDIsIkMiXSxbMSwwLCJpXzEiXSxbMiwwLCJpXzIiLDJdLFsxLDMsImYiLDJdLFsyLDMsImciXSxbMCwzLCJcXGV4aXN0cyFbZixnXSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
   \[
     \begin{tikzcd}
       A && {A+B} && B \\
       \\
       && C
-      \arrow["{i_1}", from=1-1, to=1-3]
+      \arrow["{\inl}", from=1-1, to=1-3]
-      \arrow["{i_2}"', from=1-5, to=1-3]
+      \arrow["{\inr}"', from=1-5, to=1-3]
       \arrow["f"', from=1-1, to=3-3]
       \arrow["g", from=1-5, to=3-3]
       \arrow["{\exists![f,g]}", dashed, from=1-3, to=3-3]
@@ -249,27 +249,27 @@ We can now characterize products (and later dually coproducts) as a commutative
   $1$ is a unit of $\times$, i.e.\ $A \iso A \times 1$ for any $A \in \obj{\CC}$.
 \end{proposition}
 \begin{proof}
-  Take $\langle id_A , !_A \rangle : A \to A \times 1$ and $\pi_1 : A \times 1 \to A$, this indeed constitutes an isomorphism, since
+  Take $\langle id_A , !_A \rangle : A \to A \times 1$ and $\fst : A \times 1 \to A$, this indeed constitutes an isomorphism, since
-  \[\pi_1 \comp \langle id_A , !_A \rangle = id_A \]
+  \[\fst \comp \langle id_A , !_A \rangle = id_A \]
   by definition and
-  \[\langle id_A , !_A \rangle \comp \pi_1 = \langle \pi_1 , !_A \rangle = \langle \pi_1 , \pi_2 \rangle = id_{A \times 1},\]
+  \[\langle id_A , !_A \rangle \comp \fst = \langle \fst , !_A \rangle = \langle \fst , \snd \rangle = id_{A \times 1},\]
-  because $\pi_2 = !_A : A \times 1 \to 1$ by uniqueness of $!_A$.
+  because $\snd = !_A : A \times 1 \to 1$ by uniqueness of $!_A$.
 \end{proof}
 \begin{proposition}
   $\times$ is associative, i.e.\ $A \times (B \times C) \iso (A \times B) \times C$ for any $A,B,C \in \obj{\CC}$.
 \end{proposition}
 \begin{proof}
-  Take \[\alpha = \langle \langle \pi_1 , \pi_1 \comp \pi_2 \rangle , \pi_2 \comp \pi_2 \rangle : A \times (B \times C) \to (A \times B) \times C\]
+  Take \[\alpha = \langle \langle \fst , \fst \comp \snd \rangle , \snd \comp \snd \rangle : A \times (B \times C) \to (A \times B) \times C\]
-  and \[\alpha^{-1} = \langle \pi_1 \comp \pi_1 , \langle \pi_2 \comp \pi_1 , \pi_2 \rangle \rangle : (A \times B) \times C \to A \times (B \times C).\]
+  and \[\alpha^{-1} = \langle \fst \comp \fst , \langle \snd \comp \fst , \snd \rangle \rangle : (A \times B) \times C \to A \times (B \times C).\]
   The rest of the proof then amounts to simply rewriting.
 \end{proof}
 \begin{proposition}
   $\times$ is commutative, i.e.\ $A \times B \iso B \times A$ for any $A, B \in \obj{\CC}$.
 \end{proposition}
 \begin{proof}
-  Take \[\langle \pi_2 , \pi_1 \rangle : A \times B \to B \times A\]
+  Take \[\langle \snd , \fst \rangle : A \times B \to B \times A\]
-  and \[\langle \pi_2 , \pi_1 \rangle : B \times A \to A \times B.\]
+  and \[\langle \snd , \fst \rangle : B \times A \to A \times B.\]
-  Indeed, $\langle \pi_2 , \pi_1 \rangle \comp \langle \pi_2 , \pi_1 \rangle = \langle \pi_2 \comp \langle \pi_2 , \pi_1 \rangle , \pi_1 \comp \langle \pi_2 , \pi_1 \rangle \rangle = \langle \pi_1 , \pi_2 \rangle = id$.
+  Indeed, $\langle \snd , \fst \rangle \comp \langle \snd , \fst \rangle = \langle \snd \comp \langle \snd , \fst \rangle , \fst \comp \langle \snd , \fst \rangle \rangle = \langle \fst , \snd \rangle = id$.
 \end{proof}
 
 Duality instantly yields the commutative monoid structure of coproducts:
@@ -334,7 +334,7 @@ We can however consider structures like products and isomorphisms in the quasi-c
     \item $\obj{\CC \times \CD} = \obj{\CC} \times \obj{\CD}$,
     \item $(\CC \times \CD)((A_1, A_2),(B_1,B_2)) = \CC(A_1, B_1) \times D(A_2, B_2)$,
   \end{itemize}
-  with projection functors $\pi_1 : \CC \times \CD \to \CC, \pi_2 : \CC \times \CD \to \CD$.
+  with projection functors $\fst : \CC \times \CD \to \CC, \snd : \CC \times \CD \to \CD$.
 \end{definition}
 \begin{example} More examples of functors include:
   \begin{enumerate} \setcounter{enumi}{\value{resumeenum}}
@@ -895,7 +895,7 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
               \arrow["zip"', from=1-1, to=3-1]
               \arrow["{\langle hd , tl \rangle}"', from=3-1, to=3-4]
               \arrow["{id \times zip}", from=1-4, to=3-4]
-              \arrow["{\langle hd \comp \pi_1 , \langle \pi_2 , tl \comp \pi_1 \rangle \rangle}", from=1-1, to=1-4]
+              \arrow["{\langle hd \comp \fst , \langle \snd , tl \comp \fst \rangle \rangle}", from=1-1, to=1-4]
             \end{tikzcd}\]
     \item Similarly, for $f : A \rightarrow B$ we can define $map\;f : A^\omega \to B^\omega$ by
           \[hd(map\;f\;as) = f(hd\;as); \qquad tl(map\;f\;as) = map\;f\;(tl\;as),\]
@@ -919,9 +919,65 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
   \[(C,c) \overset{h}{\longrightarrow} (E,e) \overset{k}{\longleftarrow} (D,d),\]
   such that $h\;x = k\;y$.
 \end{definition}
-% TODO if \nu F exists, ...
+
-% TODO bisimilarity
+\begin{remark}
-% TODO proof bisimilar \to \sim, etc
+  If $\nu F$ exists then
-% TODO examples of bisimilarity
+  \[x \sim y \iff h_c\;x = h_d\;y,\]
+  where $h_c : (C,c) \to (\nu F, t), h_d : (D,d) \to (\nu F, t)$ are the unique morphisms into the terminal coalgebra.
+  The proof of ``$\Leftarrow$'' is clear, for ``$\Rightarrow$'' consider the diagram:
+  % https://q.uiver.app/#q=WzAsNixbMCwwLCIoQywgYykiXSxbMywwLCIoRSxlKSJdLFs2LDAsIihELGQpIl0sWzMsMywiKFxcbnUgRiwgdCkiXSxbMiwxLCJcXGNvbW0iXSxbNCwxLCJcXGNvbW0iXSxbMCwxLCJoIl0sWzIsMSwiayIsMl0sWzAsMywiaF9jIiwyXSxbMiwzLCJoX2QiXSxbMSwzLCJoX2UiLDJdXQ==
+  \[\begin{tikzcd}
+      {(C, c)} &&& {(E,e)} &&& {(D,d)} \\
+      && \comm && \comm \\
+      \\
+      &&& {(\nu F, t)}
+      \arrow["h", from=1-1, to=1-4]
+      \arrow["k"', from=1-7, to=1-4]
+      \arrow["{h_c}"', from=1-1, to=4-4]
+      \arrow["{h_d}", from=1-7, to=4-4]
+      \arrow["{h_e}"', from=1-4, to=4-4]
+    \end{tikzcd}\]
+\end{remark}
+\begin{example}
+  As a consequence of the previous remark, we can follow that for $FX = 2 \times X^\Sigma$ the following holds:
+  \[x \sim y \iff x,y accept the same formal language.\]
+\end{example}
+
+\begin{definition}[Bisimulation]
+  Let $F : \Set \to \Set$ and let $(C,c), (D,d)$ be F-coalgebras. A \emph{bisimulation} is a relation $R \subseteq C \times C$ such that a coalgebra $(R, r)$ exists where
+  % https://q.uiver.app/#q=WzAsOCxbMCwwLCJDIl0sWzAsMiwiRkMiXSxbMiwwLCJSIl0sWzIsMiwiRlIiXSxbNCwwLCJEIl0sWzQsMiwiRkQiXSxbMSwxLCJcXGNvbW0iXSxbMywxLCJcXGNvbW0iXSxbMCwxLCJjIl0sWzIsMywiciJdLFs0LDUsImQiXSxbMiwwLCJcXHBpXzEiLDJdLFsyLDQsIlxccGlfMiJdLFszLDEsIkZcXHBpXzEiLDJdLFszLDUsIkZcXHBpXzIiXV0=
+  \[\begin{tikzcd}
+      C && R && D \\
+      & \comm && \comm \\
+      FC && FR && FD
+      \arrow["c", from=1-1, to=3-1]
+      \arrow["r", from=1-3, to=3-3]
+      \arrow["d", from=1-5, to=3-5]
+      \arrow["{\fst}"', from=1-3, to=1-1]
+      \arrow["{\snd}", from=1-3, to=1-5]
+      \arrow["{F\fst}"', from=3-3, to=3-1]
+      \arrow["{F\snd}", from=3-3, to=3-5]
+    \end{tikzcd}\]
+  commutes.
+  Two elements $c \in C, d \in D$ are called \emph{bisimilar} if there exists a bisimulation $R$ such that $xRy$ holds.
+\end{definition}
+
+\begin{proposition}
+  \[x,y \text{ bisimilar} \Rightarrow x \sim y\]
+\end{proposition}
+% TODO proof and backwards direction.
+
+\begin{example}
+  Let us examine bisimilarity of streams, i.e.\ consider the functor $FX = A \times X$ and coalgebras
+  \[C \overset{\langle h , t \rangle}{\longrightarrow} A \times C; \qquad D \overset{\langle h', t'\rangle}{\longrightarrow} A \times D.\]
+  A relation $R \subseteq C \times D$ is a bisimulation if
+  \begin{itemize}
+    \item $h\;x = h'\;y$,
+    \item $xRy \Rightarrow (t\;x)R(t'\;y)$.
+  \end{itemize}
+
+  % TODO example proof, needs some interesting functions introduced earlier.
+\end{example}
+
 \section{Limits}
 \section{Colimits}