Work on bisimilarity

tex/sections/02_categories.tex

@@ -944,7 +944,7 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
 \end{example}
 
 \begin{definition}[Bisimulation]
-  Let $F : \Set \to \Set$ and let $(C,c), (D,d)$ be F-coalgebras. 
+  Let $F : \Set \to \Set$ and let $(C,c), (D,d)$ be F-coalgebras.
   A \emph{bisimulation} is a relation $R \subseteq C \times D$ such that a coalgebra $(R, r)$ exists where
   % https://q.uiver.app/#q=WzAsOCxbMCwwLCJDIl0sWzAsMiwiRkMiXSxbMiwwLCJSIl0sWzIsMiwiRlIiXSxbNCwwLCJEIl0sWzQsMiwiRkQiXSxbMSwxLCJcXGNvbW0iXSxbMywxLCJcXGNvbW0iXSxbMCwxLCJjIl0sWzIsMywiciJdLFs0LDUsImQiXSxbMiwwLCJcXHBpXzEiLDJdLFsyLDQsIlxccGlfMiJdLFszLDEsIkZcXHBpXzEiLDJdLFszLDUsIkZcXHBpXzIiXV0=
   \[\begin{tikzcd}
@@ -963,9 +963,53 @@ Dual to F-algebras the \emph{initial F-coalgebra} is trivial:
   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}
+\begin{proposition} Let $\CC$ be a category that has pushouts, then
   \[x,y \text{ bisimilar} \Rightarrow x \sim y\]
 \end{proposition}
+\begin{proof}
+  Let $x \in (C,c)$ and $y \in (D,d)$ be bisimilar with the bisimilarity $R \subseteq C \times D$.
+  Since $\CC$ has pushouts, also $\Alg{F}$ has pushouts.
+  Consider the following pushout:
+  % https://q.uiver.app/#q=WzAsNSxbMSwwLCIoUixyKSJdLFsyLDEsIihELGQpIl0sWzAsMSwiKEMsYykiXSxbMSwyLCIoUCxwKSJdLFsxLDEsIlxcY29tbSJdLFswLDIsIlxccGlfMSIsMl0sWzAsMSwiXFxwaV8yIl0sWzIsMywiaF9jIiwyXSxbMSwzLCJoX2QiXSxbMywwLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyLWludmVyc2UifX1dXQ==
+  \[\begin{tikzcd}
+      & {(R,r)} \\
+      {(C,c)} & \comm & {(D,d)} \\
+      & {(P,p)}
+      \arrow["{\pi_1}"', from=1-2, to=2-1]
+      \arrow["{\pi_2}", from=1-2, to=2-3]
+      \arrow["{h_c}"', from=2-1, to=3-2]
+      \arrow["{h_d}", from=2-3, to=3-2]
+      \arrow["\ulcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=3-2, to=1-2]
+    \end{tikzcd}\]
+  It thus suffices to show that $h_c(x) = h_d(y)$, which indeed follows by the pushout diagram:
+  \[h_c(x) = h_c(\pi_1(x,y)) = h_d(\pi_2(x,y)) = h_d(y).\]
+\end{proof}
+
+\begin{proposition}
+  If the terminal F-coalgebra $\nu F$ exists, then
+  \[x,y \text{ bisimilar} \Rightarrow x \sim y\]
+\end{proposition}
+\begin{proof}
+  Consider the diagram
+  % https://q.uiver.app/#q=WzAsNCxbMCwxLCIoQyxjKSJdLFsxLDAsIihSLHIpIl0sWzIsMSwiKEQsZCkiXSxbMSwyLCIoXFxudSBGLHQpIl0sWzEsMCwiXFxwaV8xIiwyXSxbMSwyLCJcXHBpXzIiXSxbMCwzLCJoX2MiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJoX2QiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMSwzLCJoX3AiLDIseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
+  \[\begin{tikzcd}
+      & {(R,r)} \\
+      {(C,c)} && {(D,d)} \\
+      & {(\nu F,t)}
+      \arrow["{\pi_1}"', from=1-2, to=2-1]
+      \arrow["{\pi_2}", from=1-2, to=2-3]
+      \arrow["{h_c}"', dashed, from=2-1, to=3-2]
+      \arrow["{h_d}", dashed, from=2-3, to=3-2]
+      \arrow["{h_p}"', dashed, from=1-2, to=3-2]
+    \end{tikzcd}\]
+  Again, since $x$ and $y$ are bisimilar we get
+  \[h_c(x) = h_c(\pi_1(x,y)) = h_d(\pi_2(x,y)) = h_d(y).\]
+\end{proof}
+\begin{remark}
+  Bisimilarity of elements of the terminal F-coalgebra is equivalent to equality,
+  since then $R \subseteq \Delta = \{(x,x)\;\vert\;x\in \nu F\}$,
+  because in this case $\pi_1 = \pi_2$, by uniqueness of the morphism into the terminal F-coalgebra.
+\end{remark}
 % TODO proof and backwards direction.
 
 \begin{example}