pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

a small prop

Browse Source
This commit is contained in:
partowp 2026-04-29 14:58:33 +01:00
parent e9bc1cba67
commit 206e1ef59b
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
draft/draft.tex
View File

@ -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}