diff --git a/draft/draft.tex b/draft/draft.tex index 3f06dec..2896c35 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -725,22 +725,22 @@ From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ %\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 + For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R'\subseteq X_1\times X_2$ and a bijection $r\c R\to R'$, 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. + By~\autoref{prop:joint-mon-pair} since $\Set$ has products $\brks{p_1,p_2}$ is monic. We take $R'$ as the image of $\brks{p_1,p_2}$ and we take $r\c R\to R'$ 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$, + For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R'\subseteq X_1\times X_2$ and an bijection $r\c R\to R'$, such that for every $(x_1,x_2)\in R'$, \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 + The mentioned $r$ exists by~\autoref{lem:rel-iso}. For every $(x_1,x_2)\in R'$ 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} @@ -755,7 +755,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and % =&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: + $(\Rightarrow)$: By~\autoref{lem:rel-iso} there exist bijections $r\c R\to R'$ and $s\c S\to S'$ 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'$ we have $(g_1(x_1),g_2(x_2))\in S'$. So, we define $w'\c R'\to S'$ 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*} q_i\comp w(u)\\ =&q_i\comp s^\mone\comp w'\comp r(u)\\ @@ -786,7 +786,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and \end{proof} \begin{prop}\label{prop:rel-spa} - 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 $\spa$, 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$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel$. + 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 $\spa$, 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$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel$. \end{prop} \begin{proof} Trivial by the definitions.\qed @@ -806,7 +806,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and $\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 exists, in $\Set$.} + \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{notation} @@ -1233,7 +1233,7 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta %\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}\\ %-------------------------------------------------------------- \begin{definition}[Aczel-Mendler Bisimulation] - In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ 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)$. + Given an arbitrary category $\BC$, an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa(\BC)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ 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)$. \end{definition} % %\begin{definition}[Relation Lifting] @@ -1322,11 +1322,11 @@ We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes \end{equation*} % \begin{definition}[Hermida-Jacobs Bisimulation] - In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ 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)$. + Given a regular category $\BC$, an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, whenever there exists a morphism in $\rel(\BC)$ 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)$. \end{definition} % \begin{lemma}\label{lem:morph-spa-rel} - In a regular category $\BC$ with the axiom of choice, assuming that $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$ is an object in $\spa(\BC)$, if for an object $A$ in $\BC$ we have a morphism $w\c A\to S^\dagger$, then there exist a morphism $v\c A\to S$ such that for $i\in\{1,2\}$, we have $q_i\comp v=q_i^\dagger\comp w$. + In a regular category $\BC$ with the axiom of choice, assuming that $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$ is an object in $\spa(\BC)$, if for an object $A$ in $\BC$ we have a morphism $w\c A\to S^\dagger$, then there exists a morphism $v\c A\to S$ such that for $i\in\{1,2\}$, we have $q_i\comp v=q_i^\dagger\comp w$. \end{lemma} \begin{proof} Having the axiom of choice in a regular category $\BC$ means that for $e_S\c S\to S^\dagger$ there exist a section $s$. We define $v=s\comp w$, then for $i\in\{1,2\}$ we have: @@ -1355,14 +1355,34 @@ We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes %\end{proof} % \begin{prop}\label{prop:HeJ-AM} + Given a regular category $\BC$, we have the following: \begin{enumerate} - \item Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an AM-bisimulation on coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is a HJ-bisimulation. - \item In a regular category $\BC$ with the axiom of choice, assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a HJ-bisimulation on coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an AM-bisimulation. + \item If an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an AM-bisimulation on $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an HJ-bisimulation. + \item If every regular epimorphism in $\BC$ has a section, assuming an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an HJ-bisimulation on $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an AM-bisimulation. \end{enumerate} \end{prop} \begin{proof} - $(1)$: Trivial.\\ - $(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\qed + $(1)$: The proof is trivial if we define the witness $\sigma^\dagger\c R\to(FR)^\dagger$, such that $\sigma^\dagger=e_{FR}\comp\sigma$, where $e_{FR}$ is the epimorphism in the epi-mono factorization of $\brks{Fp_1,Fp_2}$, as depicted in the following commutative diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& Y \\ + FX \& FR \& FY \\ + FX \& {(FR)^\dagger} \& 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["\id"', from=2-1, to=3-1] + \arrow["{Fp_1}", from=2-2, to=2-1] + \arrow["{Fp_2}"', from=2-2, to=2-3] + \arrow["{e_{FR}}", from=2-2, to=3-2] + \arrow["\id", from=2-3, to=3-3] + \arrow["{Fp_1^\dagger}", from=3-2, to=3-1] + \arrow["{Fp_2^\dagger}"', from=3-2, to=3-3] + \end{tikzcd} + \end{equation*} + $(2)$: Since $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an HJ-bisimulation we have a morhpism $(\alpha,\beta,\sigma^\dagger)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp^\dagger_1}{\leftarrow} (FR)^\dagger \stackrel{Fp^\dagger_2}{\to}FY)$ in $\rel(\BC)$. By~\autoref{lem:morph-spa-rel}, there exists $\sigma\c R\to FR$ such that $(\alpha,\beta,\sigma)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ is a morphism in $\rel(\BC)$.\qed \end{proof} % \subsection{Coalgebraic Bisimulation in Set} @@ -1379,9 +1399,9 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi \begin{prop} In $\Set$, for $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, \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.\ppnote{The proof should be revised with the revision in the definition of $\rel$} + \item Assuming the axiom of choice an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa$ is an Aczel-Mendler bisimulation iff it is a span-based bisimulation. + \item An object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ is a Hermida-Jacobs bisimulation iff it is a Hughes-Jacobs bisimulation. + \item An object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation. \end{enumerate} \end{prop} \begin{proof} @@ -1389,8 +1409,8 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi (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 $(x,y)\in R$ 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 $(x,y)\in R$ there then $(\alpha(x),\beta(y))\in(FR)^\dagger$ that means that exists $u\in FR$ such that $Fp_1(u)=\alpha(x)$ and $Fp_2(u)=\beta(u)$, and it exactly means that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based 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. \qed \end{proof} \begin{cor} @@ -1452,7 +1472,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi % \begin{definition}[Hermida-Jacobs Simulation] Assuming that $\appr$ is a natural order structure on a functor $F\c\BC\to\BC$, an $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\rel(\BC)$ is a \emph{Hermida-Jacobs simulation} from a coalgebra $(X,\alpha)$ to $(Y,\beta)$, whenever the following diagram commutes laxly: - \begin{equation*}\label{eq:diag-hj-sim} + \begin{equation}\label{eq:diag-hj-sim} \begin{tikzcd}[ampersand replacement=\&] X \& R \& Y \\ FX \& (FR)^\dagger \& FY @@ -1466,18 +1486,55 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi \arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1] \arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3] \end{tikzcd} - \end{equation*} + \end{equation} \end{definition} % \begin{prop} + In a regular category $\BC$ the following propositions hold: \begin{enumerate} - \item Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$\sgnote{Is it a relation or a general span?} is an AM-simulation from a coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is a HJ-simulation. - \item In a regular category $\BC$ with the axiom of choice, assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a HJ-simulation from a coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an AM-simulation. + \item Assuming an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an AM-simulation from an $F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an HJ-simulation. + \item In a regular category $\BC$ with the axiom of choice, assuming an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an HJ-simulation from an $F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an AM-simulation. \end{enumerate} \end{prop} \begin{proof} - $(1)$: Trivial.\sgnote{Does not look so trivial.}\\ - $(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\sgnote{Add more details.}\qed + $(1)$: + We have the following lax commutative diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& Y \\ + FX \& FR \& FY \\ + FX \& {(FR)^\dagger} \& FY + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["\sqsubseteq"{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["\beta", from=1-3, to=2-3] + \arrow["\id"', from=2-1, to=3-1] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["{Fp_1}", from=2-2, to=2-1] + \arrow["{Fp_2}"', from=2-2, to=2-3] + \arrow["{e_{FR}}", from=2-2, to=3-2] + \arrow["\id", from=2-3, to=3-3] + \arrow["{Fp_1^\dagger}", from=3-2, to=3-1] + \arrow["{Fp_2^\dagger}"', from=3-2, to=3-3] + \end{tikzcd} + \end{equation*} + We define $\sigma^\dagger\c R\to(FR)^\dagger$ such that $\sigma^\dagger=e_{FR}$. Then we have + \begin{align*} + \alpha\comp p_1&\\ + &\appr Fp_1\comp\sigma\\ + &=(Fp_1)^\dagger\comp e_{FR}\comp\sigma\\ + &=(Fp_1)^\dagger\comp \sigma^\dagger, + \end{align*} + and + \begin{align*} + Fp_2\comp\sigma&\\ + &=(Fp_2)^\dagger\comp e_{FR}\comp\sigma\\ + &=(Fp_2)^\dagger\comp\sigma^\dagger\\ + &\appr\beta\comp p_2 + \end{align*} + $(2)$: Since $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an HJ-simulation we have a morhpism $\sigma^\dagger\c R\to(FR)^\dagger$ that laxly commutes in~\eqref{eq:diag-hj-sim}. By~\autoref{lem:morph-spa-rel}, there exists $\sigma\c R\to FR$ that laxly commutes in~\eqref{eq:diag-am-sim}.\qed \end{proof} % \subsection{Simulations in Set} @@ -1570,19 +1627,20 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section \end{example} % \begin{example} - 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 this relator with $\tilde{F}$. + 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}$. \end{example} % \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.\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$} + \item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\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. \end{enumerate} \end{prop} \begin{proof} - (1): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a Hermida-Jacobs simulation means that for every $(x,y)\in R$, we have $\alpha\comp p_1(x,y)\appr(Fp_1)^\dagger\comp\sigma(x,y)$ and $(Fp_2)^\dagger\comp\sigma(x,y)\appr\beta\comp p_2(x,y)$. So, $x\mathrel{R}y$ gives that $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means that $R$ is a $\tilde{F}$-simulation.\\ - (2): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a $\tilde{F}$-simulation means that $x\mathrel{R}y$ gives $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means for every $(x,y)\in R$, there exist $(u,v)\in(FR)^\dagger$ such that $\alpha(x)\appr u$ and $v\appr\beta(y)$. We form a function $f\c R\to\powf(FR)^\dagger$ such that takes every $(x,y)$ to the set of the mentioned existing pairs $(u,v)$ in $(FR)^\dagger$. By the axiom of choice there exist a function $s\c\im_f\to(FR)^\dagger$. So, assuming that $f$ has the epi-mono factorization $(e,m)$, then we define $\sigma\c R\to(FR)^\dagger$ as $\sigma=s\comp e$. Now, the diagram~\eqref{eq:diag-hj-sim} commutes laxly for the defined $\sigma$.\qed + (1): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a Hermida-Jacobs simulation means that for every $u\in R$ that $p_1(u)=x$ and $p_2(u)=y$, we have $\alpha(x)\appr(Fp_1)^\dagger\comp\sigma(u)$ and $(Fp_2)^\dagger\comp\sigma(u)\appr\beta(y)$. Since $(FR)^\dagger\subseteq FX\times FY$, so $\sigma(u)$ is a pair $(v_1,v_2)\in(FR)^\dagger$ such that $\alpha(x)\appr v_1$ and $v_2\appr\beta(y)$, and it means that $\alpha(x)\appr\comp(FR)^\dagger\comp\appr\beta(y)$. + + (2): As $(\appr\comp(FR)^\dagger\comp\appr)\subseteq FX\times FY$, the object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ being an $\tilde{F}$-simulation means that for an arbitrary $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, we have $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means for every $u\in R$, there exist $(v_1,v_2)\in(FR)^\dagger$ such that $\alpha(x)\appr v_1$ and $v_2\appr\beta(y)$. We form a function $f\c R\to\powf(FR)^\dagger$ such that takes every $u$ to the set of the mentioned existing pairs $(v_1,v_2)$ in $(FR)^\dagger$. By the axiom of choice there exists a function $s\c\im_f\to(FR)^\dagger$. So, assuming that $f$ has the epi-mono factorization $(e,m)$, then we define $\sigma\c R\to(FR)^\dagger$ as $\sigma=s\comp e$. Now, the diagram~\eqref{eq:diag-hj-sim} commutes laxly for the defined $\sigma$ as $(Fp_1)^\dagger\comp\sigma(u)=v_1$ and $(Fp_2)^\dagger\comp\sigma(u)=v_2$.\qed \end{proof} \begin{rem} The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators. @@ -4450,7 +4508,7 @@ Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed \end{proof} \begin{cor} - Recalling~\autoref{prop:left-lax-inc-triv}, for a functor $F\c\Set\to\Set$, assuming that $F^\leftarrow\leq\bar{F}$, we get $F^\leftarrow=\bar{F}$. So, if $r$ is symmetric, and it is a $F^\leftarrow$-simulation, then it is a $\bar{F}$-bisimulation. + Recalling~\autoref{prop:left-lax-inc-triv}, for a functor $F\c\Set\to\Set$, assuming that $F^\leftarrow\leq\bar{F}$, we get $F^\leftarrow=\bar{F}$. So, if $r$ is symmetric, and it is a $F^\leftarrow$-simulation, then it is a $\bar{F}$-bisimulation.ss \end{cor} \end{document}