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

diags

Browse Source
This commit is contained in:
partowp
2026-09-24 15:59:28 +01:00
parent fc57a27811
commit 1c04675e0a
1 changed files with 182 additions and 64 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+182 -64
View File
@@ -792,23 +792,51 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
\begin{proof} \begin{proof}
Trivial by the definitions.\qed Trivial by the definitions.\qed
\end{proof} \end{proof}
%\begin{figure}[t]
% \centering
% \begin{tabular}{|l|c|c|c|c|}
% \hline
% \quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\
% \hline
% $\spa$ & & & & \\
% \hline
% $\rel$ & & & & \\
% \hline
% $\spa_a$ & \ding{56} & & & \\
% \hline
% $\rel_a$ & & & & \\
% \hline
% \end{tabular}
% \caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column is in $\Set$.}
% \label{fig:anonymous_onymous-choice}
%\end{figure}
\begin{figure}[t] \begin{figure}[t]
\centering \centering
\begin{tabular}{|l|c|c|c|c|} \begin{tikzpicture}[
\hline scale=0.6, every node/.style={transform shape}
\quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\ ]
\hline \matrix (m) [matrix of nodes,
$\spa$ & & & & \\ nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
\hline align=center, font=\scriptsize, inner sep=2pt},
$\rel$ & & & & \\ row sep=6mm, column sep=6mm]
\hline {
$\spa_a$ & \ding{56} & & & \\ $\spa$ & $\spa_a$ \\
\hline $\rel$ & $\rel_a$ \\
$\rel_a$ & & & & \\ };
\hline
\end{tabular} % Example arrows (uncomment / edit as needed):
\caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column is in $\Set$.} \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-1-2);
\label{fig:anonymous_onymous-choice} \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] node[midway, above] {AC} (m-1-1);
\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] (m-2-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-2-1);
\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-2-1);
\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] (m-1-1);
\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-1-2);
\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] (m-2-2);
%
\end{tikzpicture}
\caption{Summery of results in this section about when we have a morphism in the source of an arrow then we have a morphism in the target in $\Set$.}
\label{fig:morph-summery}
\end{figure} \end{figure}
%\begin{notation} %\begin{notation}
% In the literature it is common to see a category that has sets as objects, and binary relations as morphims. Here we denote this category $\rel'$. % In the literature it is common to see a category that has sets as objects, and binary relations as morphims. Here we denote this category $\rel'$.
@@ -1411,7 +1439,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
(2): Follows from~\autoref{prop:rel-rela}. (2): Follows from~\autoref{prop:rel-rela}.
(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then by the assumption there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\\ (3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then by the assumption there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\\
($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then there exists $v^\dagger\in(FR)^\dagger$ such that $(Fp_1)^\dagger(v^\dagger)=\alpha(x)$ and $(Fp_2)^\dagger(v^\dagger)=\beta(y)$, and since $(FR)^\dagger$ by definition is the image of $\brks{Fp_1,Fp_2}$, so $(FR)^\dagger\subseteq FX\times FY$ that entails $v^\dagger=(\alpha(x),\beta(y))$. Furthemore, since $(\alpha(x),\beta(y))\in(FR)^\dagger$, there exists $v\in FR$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, so we the morphism that we want to be able to say that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation. ($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then there exists $v^\dagger\in(FR)^\dagger$ such that $(Fp_1)^\dagger(v^\dagger)=\alpha(x)$ and $(Fp_2)^\dagger(v^\dagger)=\beta(y)$, and since $(FR)^\dagger$ by definition is the image of $\brks{Fp_1,Fp_2}$, so $(FR)^\dagger\subseteq FX\times FY$ that entails $v^\dagger=(\alpha(x),\beta(y))$. Furthemore, since $(\alpha(x),\beta(y))\in(FR)^\dagger$, there exists $v\in FR$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, so we have the morphism that we want, to be able to say that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation.
\qed \qed
\end{proof} \end{proof}
\begin{cor} \begin{cor}
@@ -1434,22 +1462,50 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
% %
\begin{figure}[t] \begin{figure}[t]
\centering \centering
\begin{tabular}{|l|c|c|c|c|} \begin{tikzpicture}[
\hline scale=0.6, every node/.style={transform shape}
\qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\ ]
\hline \matrix (m) [matrix of nodes,
Aczel-Mendler & & & & \\ nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
\hline align=center, font=\scriptsize, inner sep=2pt},
Hermida-Jacobs & \ding{56} & & & \\ row sep=6mm, column sep=6mm]
\hline {
Span-based & \ding{56} & & & \\ Hughes-Jacobs & Hermida-Jacobs \\
\hline Span-based & Aczel-Mendler \\
Hughes-Jacobs & \ding{56} & & & \\ };
\hline
\end{tabular} % Example arrows (uncomment / edit as needed):
\caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.} \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-1-2);
\label{fig:bisim-choice} \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] (m-1-1);
\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] node[midway, below] {AC} (m-2-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-2-1);
\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-2-1);
\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] (m-1-1);
\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-1-2);
\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] node[midway, left] {AC} (m-2-2);
%
\end{tikzpicture}
\caption{Summery of results in this section about notions of bisimulation in $\Set$.}
\label{fig:bisim-summery}
\end{figure} \end{figure}
%\begin{figure}[t]
% \centering
% \begin{tabular}{|l|c|c|c|c|}
% \hline
% \qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\
% \hline
% Aczel-Mendler & & & & \\
% \hline
% Hermida-Jacobs & \ding{56} & & & \\
% \hline
% Span-based & \ding{56} & & & \\
% \hline
% Hughes-Jacobs & \ding{56} & & & \\
% \hline
% \end{tabular}
% \caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.}
% \label{fig:bisim-choice}
%\end{figure}
\section{Coalgebraic Simulation} \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.} %\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] \begin{definition}[Aczel-Mendler Simulation]
@@ -1556,36 +1612,69 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
% \caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.} % \caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.}
% \label{fig:anonymous_onymous_transposed} % \label{fig:anonymous_onymous_transposed}
%\end{figure} %\end{figure}
\begin{figure}[t]
\centering
\begin{tikzpicture}[ \begin{tikzpicture}[
scale=0.6, every node/.style={transform shape} scale=0.6, every node/.style={transform shape}
] ]
\matrix (m) [matrix of nodes, \matrix (m) [matrix of nodes,
nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
align=center, font=\scriptsize, inner sep=2pt}, align=center, font=\scriptsize, inner sep=2pt},
row sep=6mm, column sep=6mm] row sep=6mm, column sep=6mm]
{ {
AM-simulation & left-lax simulation\\ AM-simulation & left-lax simulation\\
& bi-lax simulation & mid-lax simulation \\ & bi-lax simulation & mid-lax simulation \\
HJ-simulation & left-lax simulation\\ HJ-simulation & left-lax simulation\\
}; };
% Example arrows (uncomment / edit as needed): % Example arrows (uncomment / edit as needed):
\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, above] {AC} (m-1-1); \draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, right=3pt] {AC} (m-1-1);
\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1); \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1);
\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above] {liftable} (m-2-3); \draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above=8pt] {liftable} (m-2-3);
\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2); \draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2);
\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, above] {coliftable} (m-2-3); \draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, below=8pt] {coliftable} (m-2-3);
\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2); \draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2);
\draw[-{Latex[length=2mm]}] (m-1-2) to node {liftable $\&$ coliftable} (m-2-2); \draw[-{Latex[length=2mm]}] (m-1-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2); \draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2);
\draw[-{Latex[length=2mm]}] (m-3-2) to node {liftable $\&$ coliftable} (m-2-2); \draw[-{Latex[length=2mm]}] (m-3-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2); \draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2);
\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1); \draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1);
\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2); \draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
\end{tikzpicture} \end{tikzpicture}
\caption{Summery of results in this section about notions of simulation in $\Set$.}
\label{fig:sim-summery}
\end{figure}
%\begin{center}
%\begin{tikzpicture}[
% scale=0.6, every node/.style={transform shape}
%]
%\matrix (m) [matrix of nodes,
% nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
% align=center, font=\scriptsize, inner sep=2pt},
% row sep=6mm, column sep=6mm]
%{
% AM-simulation & left-lax simulation\\
% & bi-lax simulation & mid-lax simulation \\
% HJ-simulation & left-lax simulation\\
%};
%
%% Example arrows (uncomment / edit as needed):
%\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, right=3pt] {AC} (m-1-1);
%\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1);
%\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above=8pt] {liftable} (m-2-3);
%\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2);
%\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, below=8pt] {coliftable} (m-2-3);
%\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2);
%\draw[-{Latex[length=2mm]}] (m-1-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
%\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2);
%\draw[-{Latex[length=2mm]}] (m-3-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
%\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2);
%\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1);
%\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
%
%\end{tikzpicture}
%\end{center}
Traditionally, simulations in $\Set$ are defined using relators. In this section we make a comparison on this concept with the other notions of simulation that we mentioned. Traditionally, simulations in $\Set$ are defined using relators. In this section we make a comparison on this concept with the other notions of simulation that we mentioned.
%\begin{notation} %\begin{notation}
@@ -1634,13 +1723,42 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
\end{definition} \end{definition}
% %
\begin{example} \begin{example}
Given $F\c\Set\to\Set$ the best example of a relator is the Barr relator. We have already introduced Barr relator, but we did not note it as a relator. It sends every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}Y)$. It is a symmetric relator. So, every simulation with this relator is actually a bisimulation. Given a functor $F\c\Set\to\Set$ the best example of a relator is the Barr relator. We have already introduced Barr relator, but we did not note it as a relator. It sends every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}Y)$. It is a symmetric relator. So, every simulation with this relator is actually a bisimulation.
\end{example} \end{example}
% %
\begin{example} \begin{lemma}\label{lem:rel-rep}
Given $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{q_2}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote a bi-lax Barr relator of a functor $F$ with $\tilde{F}$. Given a functor $F\c\Set\to\Set$, for every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$, we have $(FR)^\dagger=Fp_2\comp (Fp_1)^\op$.
\end{lemma}
\begin{proof}
Since $(FR)^\dagger$ is the image of $\brks{p_1,p_2}$, we have $(FR)^\dagger\subseteq FX\times FY$. For every $x\in FX$ and $y\in FY$ we have $x\mathrel{(FR)^\dagger}y$ iff there exists a unique $u\in FR$ such that $\brks{Fp_1,Fp_2}(u)=(x,y)$, and the latter holds if and only if $(x,y)=(Fp_1(u),Fp_2(u))$, and it is equivalent with saying that $x\mathrel{(FR)^\dagger}y$.\qed
\end{proof}
%
\begin{example}\label{ex:lax-rels}
Given a functor $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{(Fp_2)^\dagger}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote a bi-lax Barr relator of a functor $F$ with $\tilde{F}$.\\
Additionally, followed by~\autoref{lem:rel-rep} we have \emph{mid-lax} relator. This relator sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} Fp_2\comp\appr\comp (Fp_1)^\op \stackrel{(Fp_2)^\dagger}{\to}FY)$.
\end{example} \end{example}
% %
\begin{prop}
For an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ that $p_1$ and $p_2$ are surjective, assuming that a set-functor $F$ has a natural order structure $\appr$, the following propositions hold:
\begin{enumerate}
\item If $\appr$ is liftable, we have $Fp_2\comp\appr\comp(Fp_1)^\op\quad=\quad Fp_2\comp(Fp_1)^\op\comp\appr$
\item If $\appr$ is coliftable, we have $Fp_2\comp\appr\comp(Fp_1)^\op\quad=\quad \appr\comp Fp_2\comp(Fp_1)^\op$
\item If $\appr$ is both liftable and coliftable, all the following are equal:
\begin{itemize}
\item $Fp_2\comp\appr\comp(Fp_1)^\op\quad$
\item $Fp_2\comp(Fp_1)^\op\comp\appr$
\item $\appr\comp Fp_2\comp(Fp_1)^\op$
\item $\appr\comp Fp_2\comp(Fp_1)^\op\comp\appr$
\end{itemize}
\end{enumerate}
\end{prop}
\begin{proof}
They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
\end{proof}
\begin{cor}
Assuming that the order structure $\appr$ on a functor $F\c\Set\to\Set$ is liftable and coliftable, all the notions of simulation given by relators mentioned in~\autoref{ex:lax-rels}.
\end{cor}
%
\begin{prop}\label{prop:HeJ-HuJ} \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$, Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$,
\begin{enumerate} \begin{enumerate}