From 206e1ef59bce9abfccdb0c208b8859bab1a3ac1f Mon Sep 17 00:00:00 2001
From: partowp <partowp@UOB25BXTXG74.adf.bham.ac.uk>
Date: Wed, 29 Apr 2026 14:58:33 +0100
Subject: [PATCH] a small prop

---
 draft/draft.tex | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/draft/draft.tex b/draft/draft.tex
index 0ad1290..6cc5417 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -284,6 +284,7 @@
 \newcommand{\trans}{\mathsf{trans}}
 \newcommand{\preord}{\mathbf{PreOrd}}
 \newcommand{\rel}{\mathbf{Rel}}
+\newcommand{\spa}{\mathbf{Span}}
 \newcommand{\gra}{\mathbf{Gra}}
 \newcommand{\obj}{\mathbf{Obj}}
 \newcommand{\relar}{\mathbf{R}}
@@ -1936,8 +1937,17 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 \end{gather*}
 \subsection{Symmetric simulation}
 \begin{notation}
-	From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$.
+	From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$. Also, we show the category of relations over set that we represent by spans with $\spa$, and $\rel$ is the category of sets and binary relations between them.
 \end{notation}
+\begin{prop}
+	$r\c X\rto Y$ is a morphism in $\rel$ iff there is an object $(r,p_1,p_2)$ in $\spa$.
+\end{prop}
+\begin{proof}
+	($\Rightarrow$): $r\c X\rto Y$ being a morphism in $\rel$ means that in $\Set$ there exist an object $r$ with a unique mono of type $r\to X\times Y$ that is a pairing that we show with $\brks{p_1,p_2}$. So, $(r,p_1,p_2)$ form an object in $\spa$.
+	
+	($\Leftarrow$): If $(r,p_1,p_2)$ is an object in $\spa$, then $r$ is a binary relation from $X$ to $Y$ so, it is a morphism of type $X\rto Y$ in $\rel$.\qed
+\end{proof}
+The above translation seems to be true in a more general case, where $\spa$ and $\rel$ are defined on an arbitrary category (the latter is called an allegory then).
 \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}