diff --git a/draft/draft.tex b/draft/draft.tex index 0ac4459..08b029b 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1684,6 +1684,8 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio \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$. \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} \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]