diff --git a/draft/draft.tex b/draft/draft.tex
index 2b6a247..bed6a91 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -1827,34 +1827,63 @@ Abstractly, first we define an operation that we need on morphisms that takes tw
 	We have $(Fp_1)^\dagger\comp\sigma$.
 \end{proof}
 \section{Relators}
-In this section we want to discuss relators. We set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
-We answer the question that why there can be multiple simulation structures based on~\autoref{def:sim}.
+\subsection{Two-way similarity in Hughes-Jacobs}
+Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is:
+\begin{gather*}
+	\appr;(FR_1)^\dagger;\appr\quad\cap\quad\appr^\op;(FR_2)^\dagger;\appr^\op\qquad\subseteq\qquad(F(R_1\cap R_2))^\dagger
+\end{gather*}
+We need the case that $R_1=R_2$, and we refer to it with $R$. So, we need to have
+\begin{gather*}
+	\appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op\qquad\subseteq\qquad(FR)^\dagger.
+\end{gather*}
+Assuming $(x_1,x_2)\quad\in\quad	\appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op$ means that there exist $(u,v),(u',v')\in (FR)^\dagger$, such that $x_1\appr u$, $u'\appr x_1$, $v\appr x_2$, and $x_2\appr v'$. We can also use the symmetry of $R$, and then from $(x_1,x_2)\in R$ derive that there exist $(w,z),(w',z')$ such that $x_1\appr z$, $z'\appr x_1$, $w\appr x_2$, and $x_2\appr w'$. But then how can we derive $(x_1,x_2)\in (FR)^\dagger$?
+
+\todo{Investigate more! Can it be doable really?!}
+\subsection{Uniqueness of the witness in Hughes-Jacobs definition}
+In this section we set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
+We answer the question that why there can be multiple simulation witnesses based on~\autoref{def:sim}, while for the same relation, there is only one witness according to Hughes-Jacobs simulation. 
+ \begin{definition}[Hughes-Jacobs Simulation]
+	For a functor $F$, and a poset $\appr$ over $F$ a HuJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to (Fr)^\dagger$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			X \& R \& Y \\
+			{FX} \& {\appr;(FR)^\dagger;\appr} \& {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["\sigma", from=1-2, to=2-2]
+			\arrow["\beta", from=1-3, to=2-3]
+			\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
+			\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
 At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
-		X \& R \& X \\
-		{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X}
+		X \& R \& Y\\
+		{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}Y}
 		\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["\sigma", dashed, from=1-2, to=2-2]
-		\arrow["\alpha", from=1-3, to=2-3]
+		\arrow["\beta", from=1-3, to=2-3]
 		\arrow["{{\mathcal{P}p_1}_\subseteq}", from=2-2, to=2-1]
 		\arrow["{{\mathcal{P}p_2}_\subseteq}"', from=2-2, to=2-3]
 	\end{tikzcd}
 \end{equation*}
-It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\alpha(x_2))$.
+It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\beta(x_2))$.
 But $\sigma'$ in the following diagram is not unique:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
-		X \& R \& X \\
-		{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X}
+		X \& R \& Y \\
+		{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}Y}
 		\arrow["\alpha"', from=1-1, to=2-1]
 		\arrow["\subseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
 		\arrow["{p_1}"', from=1-2, to=1-1]
 		\arrow["{p_2}", from=1-2, to=1-3]
 		\arrow["{\sigma'}", from=1-2, to=2-2]
-		\arrow["\alpha", from=1-3, to=2-3]
+		\arrow["\beta", from=1-3, to=2-3]
 		\arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
 		\arrow["{{\mathcal{P}p_1^\dagger}}", from=2-2, to=2-1]
 		\arrow["{{\mathcal{P}p_2^\dagger}}"', from=2-2, to=2-3]
@@ -1863,17 +1892,17 @@ But $\sigma'$ in the following diagram is not unique:
 Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
-		X \& R \& X \\
-		{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X} \\
-		{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X}
+		X \& R \& Y \\
+		{\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}Y} \\
+		{\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}Y}
 		\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["{\sigma'}", from=1-2, to=2-2]
-		\arrow["\alpha", from=1-3, to=2-3]
+		\arrow["\beta", from=1-3, to=2-3]
 		\arrow["id"', from=2-1, to=3-1]
 		\arrow["\delta", from=2-2, to=3-2]
-		\arrow["id"', from=2-3, to=3-3]
+		\arrow["id", from=2-3, to=3-3]
 		\arrow["{{\mathcal{P}p_1}_\subseteq}", from=3-2, to=3-1]
 		\arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3]
 	\end{tikzcd}
@@ -1888,26 +1917,41 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 	u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
 	u(\inr w)=w
 \end{gather*}
+\subsection{Symmetric simulation}
 \begin{definition}[Relator]
 	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends a morphism of $\Rel$ that is a relation $X\rto Y$ to $FX\rto FY$. 
 \end{definition}
  
 \begin{definition}[Hermida-Jacobs Simulation]
-	For a relator $\relar$ for a functor $F$, and a poset $\appr$ over $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ such that the following diagram commutes ($;$ is the relation composition):
-	\begin{equation*}
+	For a relator $\relar$ on a functor $F$, and a poset $\appr$ over $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
+	\begin{equation*}\label{def:hej-sim}
 		\begin{tikzcd}[ampersand replacement=\&]
-			X \& R \& X \\
-			{FX} \& {\appr;(FR)^\dagger;\appr} \& {FX}
+			X \& R \& Y \\
+			{FX} \& {\appr;\relar r;\appr} \& {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["\sigma", from=1-2, to=2-2]
-			\arrow["\alpha", from=1-3, to=2-3]
+			\arrow["\beta", from=1-3, to=2-3]
 			\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
 			\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
 		\end{tikzcd}
 	\end{equation*}
 \end{definition}
+\begin{prop}
+	Hughes-Jacobs simulation is an instance of HJ-simulation, where $\relar r=(Fr)^\dagger$. 
+\end{prop}
+\begin{proof}
+	We need to show that $(F-)^\dagger$ is a relator, we need to show that 
+	
+	\todo{Finish.}
+\end{proof}
+\begin{prop}
+	For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a simulation, the witness is unique.
+\end{prop}
+\begin{proof}
+	It only relies on the fact that ${Fp_1}_\appr$ and ${Fp_2}_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed
+\end{proof}
 \end{document}