pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

double more

Browse Source
This commit is contained in:
partowp
2026-08-31 22:23:28 +01:00
parent c6514f23b7
commit 1458958104
1 changed files with 2 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+2
View File
@@ -1684,6 +1684,8 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
\begin{definition}[Double Coalgebra] \begin{definition}[Double Coalgebra]
Given a double category $\BC_1\rightrightarrows\BC_0$, and a $F$-double relator $\relar$, a pair $(\mathcal{R},\delta)$ is an $\relar$-double coalgebra on $\BC_1\rightrightarrows\BC_0$. Given a double category $\BC_1\rightrightarrows\BC_0$, and a $F$-double relator $\relar$, a pair $(\mathcal{R},\delta)$ is an $\relar$-double coalgebra on $\BC_1\rightrightarrows\BC_0$.
\end{definition} \end{definition}
\todo{First, finish the subsection in section 2, then come back here and continue this by saying that every relator is a double relator in $\Set$, and then define symmetric double relators, and then instantiate every notion that you have introduced in previous sections.}
\todo{Perhaps in the future you can also introduce properties of relators for double relatros.}
\section{Symmetric Simulation is a Bisimulation} \section{Symmetric Simulation is a Bisimulation}
\todo{Obviously, this chapter should be changed. All the definitions should be moved to somewhere else. You should start the chapter by giving your counter examples, and then presenting your proofs.} \todo{Obviously, this chapter should be changed. All the definitions should be moved to somewhere else. You should start the chapter by giving your counter examples, and then presenting your proofs.}
\begin{definition}[Graph] \begin{definition}[Graph]