diff --git a/draft/draft.tex b/draft/draft.tex index d635f77..cac318c 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -386,7 +386,21 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}} \end{abstract} % % - +\section{Relation Lifting} +\begin{definition}[Natural Order Structure]\label{def:nat-ord} + A \emph{natural order structure} on a functor $F$ is a poset $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then: + \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] + \item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',FY)$. \label{item:nat-ord:I} + \item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II} + \end{enumerate} +\end{definition} +We want to say that a natural order structure entails an order over a functor defined by Jacobs and Hughes that is a functor of the type $\Set\to\mathbf{Poset}$. +\begin{prop} + Assuming that $F\c\Set\to\Set$ is a functor, and we have a natural order structure on $F$, then we have a functor $\tilde{F}\c\Set\to\mathbf{Poset}$, such that $U\comp \tilde{F}=F$, where $U$ is a forgetful functor. +\end{prop} +\begin{proof} + We take $\tilde{F}X=\Hom(1,FX)$. Assuming that $U$ takes every poset to its carrier set, then we have $U\comp\tilde{F}X=FX$ for every object $X$.\qed +\end{proof} \section{Coalgebraic Bisimulation}%\label{sec:} In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\ @@ -2184,9 +2198,9 @@ Now, we prove that the given order on the maybe functor is a liftable one. The order structure on the set-functor $FX=X+1$ is a liftable order. \end{lemma} \begin{proof} - By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: + By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases: \begin{itemize} - \item $h=\bot$: In this case we take $k'=\bot$, then we have $g+1(k')=\bot=h$. + \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $g+1(k')=\bot=h$. \item $g+1(k)=h$: In this case we take $k'=k$, then we have $g+1(k')=h$, and they are both an element of $Y$.\qed \end{itemize} @@ -2250,11 +2264,57 @@ So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra (\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X \end{cases} \end{gather*} - Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.\qed + Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$. + Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $\alpha(x_i)\in X=(p_i+1)\comp\beta(x_1,x_2)$ we have $\beta(x_1,x_2)\in R$. + \qed \end{proof} +Now, we want to abstract the given proof for an arbitrary category that has coproducts and terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$. %Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one. - +\begin{lemma}\label{lem:maybe-lif-abs} + The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.\ppnote{incomplete! Say why $(\alpha(x_1),\alpha(x_2))\in R+1$.} +\end{lemma} +\begin{proof} + For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr g+1\comp k$ that means we have two cases: + \begin{itemize} + \item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $g+1\comp k'=h$. + \item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $g+1\comp k'=h$.\qed + \end{itemize} +\end{proof} +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {I_{X^2}} \& R \& {I_{(2\times X)}} \& R \\ + {X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\ + \& {I_1} \& R \\ + \& 1 \& {X^2+(2\times X)+1} + \arrow["{q_1}", from=1-1, to=1-2] + \arrow["{q_2}"', from=1-1, to=2-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] + \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-2, to=2-2] + \arrow["{r_1}", from=1-3, to=1-4] + \arrow["{r_2}"', from=1-3, to=2-3] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] + \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-4, to=2-4] + \arrow["{\mathsf{in}_1}"', from=2-1, to=2-2] + \arrow["{\mathsf{in}_2}"', from=2-3, to=2-4] + \arrow["{s_1}", from=3-2, to=3-3] + \arrow["{s_2}"', from=3-2, to=4-2] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3] + \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=3-3, to=4-3] + \arrow["{\mathsf{in}_3}"', from=4-2, to=4-3] + \end{tikzcd} +\end{equation*} +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + R \& I \& {X^2+(2\times X)+1} + \arrow["e", two heads, from=1-1, to=1-2] + \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3] + \arrow["m", tail, from=1-2, to=1-3] + \end{tikzcd} +\end{equation*} +\begin{gather*} + I\iso I_{X^2}+I_{2\times X}+I_{1} +\end{gather*} \section{Relators} \subsection{Two-way similarity in Hughes-Jacobs} Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is: @@ -2742,13 +2802,13 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \begin{proof} \todo{Finish.} \end{proof} -\begin{definition}[Natural Order Structure]\label{def:nat-ord} - A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then: - \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] - \item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',FY)$. \label{item:nat-ord:I} - \item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II} - \end{enumerate} -\end{definition} +%\begin{definition}[Natural Order Structure]\label{def:nat-ord} +% A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then: +% \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] +% \item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',FY)$. \label{item:nat-ord:I} +% \item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II} +% \end{enumerate} +%\end{definition} \begin{definition}[Liftable Order Structure]\label{def:liftable-ord} A \emph{liftable order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.