diff --git a/draft/draft.tex b/draft/draft.tex
index ba295ae..0ac4459 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -1090,7 +1090,6 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 \subsection{Bisimulation in Double Categories}
 \todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".}
 %
-
 \section{Coalgebraic Simulation}
 \todo{Give an introduction of the definitions for $\spa(\BC)$ and $\rel(\BC)$ that are AM-simulation and HJ-simulation, then open up the discussion about relators.}
 \begin{definition}[Aczel-Mendler Simulation]
@@ -1211,7 +1210,7 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 \begin{rem}
 	The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.
 \end{rem}
-\todo{Read section V of the LICS paper and see what is the non-symmetric relator. Then try to see if HJ-simulation subsumes it.}
+Having lax versions of a symmetric relator, allows us to have simulation relations that are related to bisimulation. Also, we did show in the previous proposition that making the commuting diagram lax, with the relator that is not laxed, we get an equivalent definition under the axiom of choice. But if the relator is not symmetric, it is already giving us a notion of simulation, even though we have not laxed it!
 \subsection{Simulations in Double Categories}
 \todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!}
 %We show the category of partially ordered sets with monotone functions between them with $\poset$. 
@@ -1671,6 +1670,20 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 %
 %\subsection{Choosing a suitable order for our setting}
 %Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
+\section{Simulations and Bisimulations in Double Categories}
+\begin{definition}[Double Relator]
+	Given a double category $\BC_1\rightrightarrows\BC_0$, for an endofunctor $F$, an $F$-double relator $\relar$ is a map on the objects of $\BC_1$, for which the following equations hold:
+	\begin{enumerate}
+		\item $S\comp F=\relar\comp S$
+		\item $T\comp F=\relar\comp T$
+		\item $\relar\comp U=U\comp F$
+	\end{enumerate}
+	Additionally, it takes every cell of type $\mathcal{R}\Rightarrow\mathcal{S}$ to a cell of type $\relar\mathcal{R}\Rightarrow\relar\mathcal{S}$.
+\end{definition}
+%
+\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}
 \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]