diff --git a/draft/draft.tex b/draft/draft.tex
index 2c3043f..3f06dec 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -672,7 +672,7 @@ Now, we prove $Sg(\mu') = \nu$.
 %an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
 %We define the category of spans and relations.
 \begin{definition}[Category of Spans]\ppnote{Paul Levy said he doesn't like this name for this category as "category of spans" is used for a different category that is a bicategory.}
-	For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, whenever the following diagram commutes:
+	For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ (called \emph{witness}) in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, whenever the following diagram commutes:
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			{X_1} \& R \& {X_2} \\
@@ -692,13 +692,20 @@ Now, we prove $Sg(\mu') = \nu$.
 	A pair of morphisms $p_1\c R\to X$ and $p_2\c R\to Y$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$.
 \end{definition}
 %
-\begin{prop}
+\begin{prop}\label{prop:joint-mon-unique}
+	Given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$, assuming $q_1$ and $q_2$ are jointly monic, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then $w$ is unique.\qed
+\end{prop}
+%
+\begin{prop}\label{prop:joint-mon-pair}
 	In a category $\BC$ with products, two morphisms $p_1\c R\to X$ and $p_2\c R \to Y$ are jointly monic iff $\brks{p_1,p_2}\c R\to X\times Y$ is monic.\qed   
 \end{prop}
 %
 \begin{definition}[Category of Relations]
-For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
+For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is a full subcategory of $\spa(\BC)$ such that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel(\BC)$, $p_1$ and $p_2$ are jointly monic. %A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
 \end{definition}
+\begin{remark}
+	Followed by~\autoref{prop:joint-mon-unique}, given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel(\BC)$, for morphisms $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$ in $\BC$, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then for every $v\c R\to S$, such that $(g_1,g_2,v)$ is a morphism in $\rel(\BC)$, then $v=w$. 
+\end{remark}
 %
 %\begin{prop}
 %	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel(\BC)$ and $\spa(\BC)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel(\BC)$.
@@ -709,32 +716,61 @@ For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary
 %
 \subsection{Spans and Relations in $\Set$}
 From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ accordingly. There are two choices for defining morphisms in each of the categories $\spa$ and $\rel$, namely \emph{anonymous} and \emph{onymous}. The already introduced type of morphisms is onymous. For functions $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2) \to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ is an anonymous morphism in $\spa$ if:
-\begin{gather*}
+\begin{gather}\label{eq:ano-morph}
 	u\in R\Rightarrow \exists v\in S, q_1(v)= g_1\comp p_1(u) \quad\&\quad q_2(v)=g_2\comp p_2(u)
-\end{gather*}
-	In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that  forces the elements of relations to be pairs and the existential quantifier refers to a unique element:
-\begin{gather*}
-	(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
-\end{gather*}
+\end{gather}
+%	In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that  forces the elements of relations to be pairs and the existential quantifier refers to a unique element:
+%\begin{gather*}
+%	(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
+%\end{gather*}
 From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to denote the categories of spans and relations with onymous morphisms.
+\begin{lemma}\label{lem:rel-iso}
+	For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R^\dagger\subseteq X_1\times X_2$ and an bijection $r\c R\to R^\dagger$, such that
+	\begin{gather*}
+		\forall u\in R,\; p_1(u)=x_1\;\&\; p_2(u)=x_2\iff r(u)=(x_1,x_2).
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	By~\autoref{prop:joint-mon-pair} since $\Set$ has products $\brks{p_1,p_2}$ is monic. We take $R^\dagger$ as the image of $\brks{p_1,p_2}$ and we take $r\c R\to R^\dagger$ as the epimorphism in the image factorization of $\brks{p_1,p_2}$. Since $\brks{p_1,p_2}$ is monic, $r$ is a bijection. Now, the mentioned property is trivial.
+\end{proof}
+\begin{cor}\label{cor:rel-iso}
+	For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R^\dagger\subseteq X_1\times X_2$ and an bijection $r\c R\to R^\dagger$, such that for every $(x_1,x_2)\in R^\dagger$,
+	\begin{gather*}
+		p_1\comp r^{-1}(x_1,x_2)=x_1\quad\&\quad p_2\comp r^{-1}(x_1,x_2)=x_2.
+	\end{gather*}
+\end{cor}
+\begin{proof}
+	The mentioned $r$ exists by~\autoref{lem:rel-iso}. For every $(x_1,x_2)\in R^\dagger$ there exists a unique $u\in R$ such that $r(u)=(x_1,x_2)$, and it means that $p_1(u)=x_1$ and $p_2(u)=x_2$, so we have $u=r^\mone(x_1,x_2)$ that means $p_1\comp r^\mone(x_1,x_2)=x_1$ and $p_2\comp r^\mone(x_1,x_2)=x_2$.\qed
+\end{proof}
+%
 \begin{prop}\label{prop:rel-rela}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\rel_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness\sgnote{Unique?} $w\c R\to S$.
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\rel$ and $\rel_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the unique witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
-	$(\Rightarrow):$ For every $(x_1,x_2)\in R$ we define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have:
+%	$(\Rightarrow):$ We define $w$ as $w=\brks{g_1\comp p_1,g_2\comp p_2}$. We have:
+%	\begin{align*}
+%		g_1\comp p_1(x_1,x_2)&\\
+%		=&g_1(x_1)\\
+%		=&q_1(g_1(x_1),g_2(x_2))\\
+%		=&q_1\comp w(x_1,x_2)
+%	\end{align*}
+%	Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
+	$(\Rightarrow)$: By~\autoref{lem:rel-iso} there exist bijections $r\c R\to R^\dagger$ and $s\c S\to S^\dagger$ with the mentioned property. Since $(g_1,g_2)$ is a morphism from $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, for every $(x_1,x_2)\in R^\dagger$ we have $(g_1(x_1),g_2(x_2))\in S^\dagger$. So, we define $w'\c R^\dagger\to S^\dagger$ as $w'(x_1,x_2)=(g_1(x_1),g_2(x_2))$, and we define $w\c R\to S$ as $w=s^\mone\comp w'\comp r$. For every $u\in R$ and $i\in\{1,2\}$ we have:
 	\begin{align*}
-		g_1\comp p_1(x_1,x_2)&\\
-		=&g_1(x_1)\\
-		=&q_1(g_1(x_1),g_2(x_2))\\
-		=&q_1\comp w(x_1,x_2)
+		q_i\comp w(u)\\
+		=&q_i\comp s^\mone\comp w'\comp r(u)\\
+		=&q_i\comp s^\mone\comp w'(x_1,x_2)\\
+		=&q_i\comp s^\mone(g_1(x_1),g_2(x_2))\\
+		=&g_i(x_i)&\by{\autoref{cor:rel-iso}}\\
+		=&g_i(p_i(u))\\
+		=&g_i\comp p_i(u)
 	\end{align*}
-	Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
 	
-	$(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed
+	$(\Leftarrow):$ Assuming $u\in R$ we take $w(u)\in S$ as $v$ in~\eqref{eq:ano-morph}. We have $q_1(w(u))=p_1\comp g_1(u)$ and $q_2(w(u))=p_2\comp g_2(u)$ since $(g_1,g_2,w)$ is the morphism of the mentioned type.\qed
 \end{proof}
 
 \begin{prop}\label{prop:spa-spaa}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
 	($\Rightarrow$): We need the axiom of choice to prove this statement. By the definition of anonymous morphisms, for every $u\in R$ there exists $v\in S$ such that $q_1(v)=p_1\comp g_1(u)$ and $q_2(v)=p_2\comp g_2(u)$. So, for each $u\in R$ there exists a set $V_u\in\powf S$ that its elements have the mentioned properties. We can form a function $h\c R\to \powf S$ that $h(u)=V_u$. The image of $h$ that we denote with $\im(h)$ is a family of non-empty sets. By the axiom of choice, there exists a function $s\c \im(h)\to S$. We define $w\c R\to S$ as $w=s\comp h$, then for every $u\in R$, we have $q_1\comp w(u)=g_1\comp p_1(u)$ and $q_2\comp w(u)=g_2\comp p_2(u)$.
@@ -742,13 +778,11 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 	($\Leftarrow$): Assuming $u\in R$, there exists $w(u)\in S$, and by the definition of onymous morphisms we have $q_1(w(u))=g_1\comp p_1(u)$ and $q_2(w(u))=g_2\comp p_2(u)$. \qed
 \end{proof}
 
-\begin{prop}\label{prop:rela-spaa}\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
+\begin{prop}\label{prop:rela-spaa}%\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
 \end{prop}
 \begin{proof}
-	($\Rightarrow$): Assuming that $(g_1,g_2)$ is a morphism in $\spa_a$, then for $(x_1,x_2)\in R$ there exists $v\in S$, such that $q_1(v)=g_1(x_1)$ and $q_2(v)=g_2(x_2)$. Since $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)\in\rel_a$ then the $v$ is unique and $v=(g_1(x_1),g_2(x_2))$. 
-	
-	($\Leftarrow$): As $\rel_a$ is a subcategory of $\spa_a$, this is trivial.\qed
+	It is trivial as $\rel_a$ is a full subcategory of $\spa_a$\qed
 \end{proof}
 
 \begin{prop}\label{prop:rel-spa}
@@ -1347,7 +1381,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 	\begin{enumerate}
 		\item Assuming the axiom of choice span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an Aczel-Mendler bisimulation iff it is a span-based bisimulation.
 		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is a Hughes-Jacobs bisimulation.
-		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.
+		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
 	\end{enumerate}
 \end{prop}
 \begin{proof}
@@ -1542,8 +1576,8 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 \begin{prop}\label{prop:HeJ-HuJ}
 Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$,
 	\begin{enumerate}
-		\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.
-		\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a $\tilde{F}$-simulation, assuming the axiom of choice.
+		\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
+		\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a $\tilde{F}$-simulation, assuming the axiom of choice.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
 	\end{enumerate}
 \end{prop}
 \begin{proof}