init

draft/draft.tex

@@ -424,7 +424,67 @@ We take $\rel(F)\c\rel\to\rel$ to be the functor that for an arbitrary functor $
 	\end{equation*}
 \end{prop}
 
+\begin{definition}[Aczel-Mendler Bisimulation]
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			{X} \& R \& {Y} \\
+			{FX} \& FR \& {FY}
+			\arrow["{\alpha}"', from=1-1, to=2-1]
+			\arrow["{p_1}"', from=1-2, to=1-1]
+			\arrow["{p_2}", from=1-2, to=1-3]
+			\arrow["\gamma", from=1-2, to=2-2]
+			\arrow["{\beta}", from=1-3, to=2-3]
+			\arrow["{Fp_1}", from=2-2, to=2-1]
+			\arrow["{Fp_2}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
 
+\begin{definition}[Hermida-Jacobs Bisimulation]
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			{X} \& R \& {Y} \\
+			{FX} \& (FR)^\dagger \& {FY}
+			\arrow["{\alpha}"', from=1-1, to=2-1]
+			\arrow["{p_1}"', from=1-2, to=1-1]
+			\arrow["{p_2}", from=1-2, to=1-3]
+			\arrow["\gamma", from=1-2, to=2-2]
+			\arrow["{\beta}", from=1-3, to=2-3]
+			\arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
+			\arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
+
+\begin{definition}[Hughes-Jacobs Bisimulation]
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			{X} \& R \& {Y} \\
+			{FX} \& (FR)^\dagger \& {FY}
+			\arrow["{\alpha}"', from=1-1, to=2-1]
+			\arrow["{p_1}"', from=1-2, to=1-1]
+			\arrow["{p_2}", from=1-2, to=1-3]
+			\arrow["{\beta}", from=1-3, to=2-3]
+			\arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
+			\arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
+
+\begin{definition}[Vanilla Bisimulation]
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			{X} \& R \& {Y} \\
+			{FX} \& FR \& {FY}
+			\arrow["{\alpha}"', from=1-1, to=2-1]
+			\arrow["{p_1}"', from=1-2, to=1-1]
+			\arrow["{p_2}", from=1-2, to=1-3]
+			\arrow["{\beta}", from=1-3, to=2-3]
+			\arrow["{Fp_1}", from=2-2, to=2-1]
+			\arrow["{Fp_2}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
 \todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
 
 \todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}