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

Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

Browse Source
This commit is contained in:
Sergey Goncharov
2026-07-20 14:05:37 +01:00
parent 3d36dc3293 cc4999dcb9
commit b72995139c
1 changed files with 304 additions and 168 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+304 -168
View File
@@ -292,7 +292,9 @@
\newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}} \newcommand{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}} \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}}
\newcommand{\powf}{\mathcal{P}} \newcommand{\powf}{\mathcal{P}}
\newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}}
\newcommand{\sappr}{\sqsupseteq} \newcommand{\sappr}{\sqsupseteq}
\newcommand{\Dom}{\mathsf{Dom}}
\newcommand{\simeet}{% \newcommand{\simeet}{%
\mathbin{% \mathbin{%
@@ -401,6 +403,117 @@ We want to say that a natural order structure entails an order over a functor de
\begin{proof} \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 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} \end{proof}
\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'$.
\end{definition}
\begin{definition}[Coliftable Order Structure]\label{def:coliftable-ord}
A \emph{coliftable 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$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}
\begin{lemma}\label{lem:set-ord-str}
In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure.
\end{lemma}
\begin{proof}
For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$.
Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$.
Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$.
\qed
\end{proof}
\begin{remark}\label{rem:set-ord-str-co}
The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
\end{remark}
\begin{prop}\label{prop:lift-gen-func}
For a functor $F\c\Set\to\Set$, a functor of the form $\powf F$, where $\powf$ is the powerset functor, the set inclusion is a liftable order structure.
\end{prop}
\begin{proof}
Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf FZ)$, $k\in\Hom(1,\powf FY)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf Fg(k)$, we define $k'\in\powf FY$ that that $k'=\{y\mid Fg(y)\in h\}$. We show that $k'\subseteq k$ and $\powf Fg(k')=h$.
Assuming $y\in k'$ we have $Fg(y)\in h$. Since $h\subseteq \powf Fg(k)$ we have $Fg(y)\in\powf Fg(k)$, so we have $y\in k$ that means $k'\subseteq k$.
Assuming $z\in\powf Fg(k')$, then there exists $y'\in k'$ that $z=Fg(y')$, so $z\in h$ and $\powf Fg(k')\subseteq h$.
Assuming $z\in h$, since $h\subseteq \powf Fg(k)$, then $z\in\powf Fg(k)$. So, there exists $y'\in k$ such that $Fg(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf Fg(k')$.\qed
\end{proof}
\begin{example}
In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$.
Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed
\end{example}
\begin{remark}
We give an example that justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective.
If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is not an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$,
\begin{gather*}
g(z)=
\begin{cases}
0 & z\in\mathbb{Z}^+ \\
1 & \mathsf{otherwise}
\end{cases}
\end{gather*}
then
\begin{gather*}
\powf g(A)=
\begin{cases}
\emptyset & A=\emptyset \\
\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\
\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
\{0,1\} & \mathsf{otherwise}
\end{cases}
\end{gather*}
then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
\end{remark}
\begin{remark}
We could not prove a general statement like~\autoref{prop:lift-gen-func} for coliftability even if the surgectivity of $g$ remains in the definition. Perhaps more conditions on $F$ in~\autoref{prop:lift-gen-func} are needed. Conditions like preserving surjections and unions that make the statement extremely limited, and meaningless.
\end{remark}
\begin{lemma}\label{lem:liftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
\end{proof}
\begin{lemma}\label{lem:coliftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$.
Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
\end{proof}
\section{Coalgebraic Bisimulation}%\label{sec:} \section{Coalgebraic Bisimulation}%\label{sec:}
In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has 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.\ products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
@@ -1091,7 +1204,7 @@ A big concern with this approach is that Comma Objects are defined in a 2-catego
\subsection{Choosing a suitable order for our setting} \subsection{Choosing a suitable order for our setting}
Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term. Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
\section{Symmetric Simulation is Bisimulation} \section{Symmetric Simulation is a Bisimulation}
\begin{definition}[Graph] \begin{definition}[Graph]
In a category $\BC$ a graph is a tuple $(R,X)$ of the following form: In a category $\BC$ a graph is a tuple $(R,X)$ of the following form:
\begin{equation*} \begin{equation*}
@@ -2049,6 +2162,35 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
% \end{gather*} % \end{gather*}
% We have $(Fp_1)^\dagger\comp\sigma$. % We have $(Fp_1)^\dagger\comp\sigma$.
%\end{proof} %\end{proof}
\begin{example}
And another counter-example!!!
Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. We show the functor with $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
\begin{gather*}
\alpha(x)=
\begin{cases}
\{1,2\} & x=1 \\
\{2,3\} & x=2\\
\{3\} & x=3
\end{cases}
\end{gather*}
$\sigma$ is defined as below:
\begin{gather*}
\sigma(w)=
\begin{cases}
\{(1,2),(2,2)\} & w=(1,2) \\
\{(2,1),(2,2)\} & w=(2,1) \\
\{(1,2),(2,1)\} & w=(1,1) \\
\{(2,2),(1,1)\} & w=(2,2)
\end{cases}
\end{gather*}
$R$ is symmetric, and $\sigma$ is a witness for $R$ to be an AM-simulation, but $R$ is not a bisimulation in the traditional sense because $(2,1)\in R$, and $2\to 3$, but $(3,1)$ or $(3,2)$ are not in $R$. It is easy to see that it is not an AM-bisimulation as well because we can not define a function that can serve as an evidence for it as $3$ does not appear in any pair in $R$, while it exists in $\alpha(2)$.
This counter-example also works as a counter-example for Hughes-Jacobs definition of simulation. Actually, $\appr\comp(FR)^\dagger\comp\appr=\powf X\times \powf X$, so $R\subseteq( \appr\comp(FR)^\dagger\comp\appr)$ that means that $R$ is a simulation. Worth noting that they claim that their setting works for an arbitrary category. So, unlike their definition, in the context of the relator-based definitions that only work in $\Set$, this counter-example does not live.
The mentioned ordering is not liftable. Assuming $h\in\Hom(\nats,\powfi \nats)$, $g\c \nats\to \nats$, and $k\in\Hom(\nats,\powfi \nats)$, and they are defined for every $n$ in $\nats$ as $h(n)=\{2\times n\}$, $g(n)=3\times n$, and $k(n)=\{n\}$, then $|h(n)|=|\powfi g(k(n))|=1$ that means $h\appr\powfi g\comp k$ is satisfied, but there is no $k'$ that $h=\powfi g\comp k$ because we can never have $h(1)=\powfi g\comp k'(1)$, as assuming $k'(1)=\{n\}$, and $n$ must be a natural number, then we should have $2=3\times n$ that is impossible.
\end{example}
\subsection{The concrete proof} \subsection{The concrete proof}
%\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.} %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
% Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have: % Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
@@ -2192,18 +2334,26 @@ Now, we prove our main statement.
\end{cor} \end{cor}
Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
\subsection{Maybe Functor} \subsection{Maybe Functor}
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_{X+1}\cup\{(\bot,x)\mid x\in X\}$.\\ We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$, and for every $x\in\Dom(f)$ we have $f(x)=g(x)$ ($\Dom(f)$ is the domain of a function $f$).
Now, we prove that the given order on the maybe functor is a liftable one. Now, we prove that the given order on the maybe functor is liftable and coliftable.
\begin{lemma}\label{lem:maybe-lif} \begin{lemma}\label{lem:maybe-lif}
The order structure on the set-functor $FX=X+1$ is a liftable order. The order structure on the set-functor $FX=X+1$ is a liftable order.
\end{lemma} \end{lemma}
\begin{proof} \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 Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(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 Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
\begin{itemize} % \begin{itemize}
\item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$. % \item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
% \item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
\item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed % \end{itemize}
\end{itemize} Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$. We define $k'\in\Hom(X,Y+1)$ as follows:
\begin{gather*}
k'(x)=
\begin{cases}
\bot&x\notin\Dom(h)\\
k(x)&x\in\Dom(h)
\end{cases}
\end{gather*}
We have $\Dom((g+1)\comp k')=\Dom(k')$ and $\Dom(k')=\Dom(h)$, so we have $\Dom((g+1)\comp k')=\Dom(h)$. If $x\in\Dom(h)$, then $h(x)=(g+1)\comp k(x)$ and $(g+1)\comp k(x)=(g+1)\comp k'(x)$, so we have $h(x)=(g+1)\comp k'(x)$. So, we have $h=(g+1)\comp k'$. Additionally, $\Dom(k')\subseteq\Dom(k)$, and for every $x\in \Dom(k')$, we have $k'(x)=k(x)$, so we have $k'\appr k$. \qed
\end{proof} \end{proof}
\begin{lemma}\label{lem:maybe-colif} \begin{lemma}\label{lem:maybe-colif}
The order structure on the set-functor $FX=X+1$ is a coliftable order. The order structure on the set-functor $FX=X+1$ is a coliftable order.
@@ -2286,41 +2436,79 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
% 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 $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$. % 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 $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$.
% \qed % \qed
%\end{proof} %\end{proof}
%%%%%%Second proof:
\begin{prop}\label{prop:sym-sim-bis-may} \begin{prop}\label{prop:sym-sim-bis-may}
For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation. For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation.
\end{prop} \end{prop}
\begin{proof} \begin{proof}
We prove that $\sigma$ also is a witness for $R$ to be an AM-bisimulation. For every $(x_1,x_2)\in R$ we have We prove that $\sigma$ also is a witness for $R$ to be an AM-bisimulation. For every $(x_1,x_2)\in R$ we have
\begin{enumerate} % \begin{enumerate}
\item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}, % \item $\alpha(x_1)=(p_1+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
\item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\ % \item $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
% \end{enumerate} % % \end{enumerate}
and since $R$ is symmetric, we have % and since $R$ is symmetric, we have
% \begin{enumerate} % % \begin{enumerate}
\item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}, % \item $\alpha(x_2)=(p_1+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
\item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}, % \item $\alpha(x_1)\sappr (p_2+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
\end{enumerate} % \end{enumerate}
Followed by $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$ we have the following cases: % Followed by $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$ we have the following cases:
\begin{itemize} % \begin{itemize}
\item $\alpha(x_2)=p_2+1\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation. % \item $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation.
\item $Fp_2\comp\sigma(x_1,x_2)=\bot$: In this case, we have % \item $p_2+1\comp\sigma(x_1,x_2)=\bot$: In this case, we have
\begin{align*} % \begin{align*}
p_2+1\comp\sigma(x_1,x_2)=\bot,&\\ % (p_2+1)\comp\sigma(x_1,x_2)=\bot,&\\
\Rightarrow&\sigma(x_1,x_2)=\bot,\\ % \Rightarrow&\sigma(x_1,x_2)=\bot,\\
\Rightarrow&p_1+1\comp\sigma(x_1,x_2)=\bot,\\ % \Rightarrow&(p_1+1)\comp\sigma(x_1,x_2)=\bot,\\
\Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\ % \Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\
\Rightarrow&p_2+1\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\ % \Rightarrow&(p_2+1)\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\
\Rightarrow&\sigma(x_2,x_1)=\bot,\\ % \Rightarrow&\sigma(x_2,x_1)=\bot,\\
\Rightarrow&p_1+1\comp\sigma(x_2,x_1)=\bot,\\ % \Rightarrow&(p_1+1)\comp\sigma(x_2,x_1)=\bot,\\
\Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\ % \Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\
\Rightarrow&\alpha(x_2)=p_1+1\comp\sigma(x_1,x_2). % \Rightarrow&\alpha(x_2)=(p_1+1)\comp\sigma(x_1,x_2).
\end{align*} % \end{align*}
\end{itemize}\qed % \end{itemize}\qed
\begin{enumerate}
\item $\alpha\comp p_1=(p_1+1)\comp\sigma$\label{eq:maybe-func-set-1},
\item $\alpha\comp p_2\sappr (p_2+1)\comp\sigma$\label{eq:maybe-func-set-2},\\
and since $R$ is symmetric, we have
\end{enumerate}
Followed by~\eqref{eq:maybe-func-set-2} for every $(x_1,x_2)\in R$ we have $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$ and $\Dom((p_2+1)\comp\sigma)\subseteq\Dom(\alpha\comp p_2)$. We have
\begin{align*}
\Dom((p_2+1)\comp\sigma)&\\
=&\Dom(\sigma)\\
=&\Dom((p_1+1)\comp\sigma)\\
=&\Dom(\alpha\comp p_1)&\by{\eqref{eq:maybe-func-set-1}}\\
=&\Dom(\alpha\comp p_1\comp s)\\
=&\Dom(\alpha\comp p_2)
\end{align*}
So, we have $\alpha\comp p_2= (p_2+1)\comp\sigma$ as well that means that $\sigma$ also serves as a witness for $R$ to be a bisimulation.
\end{proof} \end{proof}
Now, we want to abstract the given proof for an extensive category that has 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$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.} Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. We use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$.%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$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.}
%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. %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.
The following lemma is an abstraction of saying that in $\Set$ assuming $f\c X\to Y+1$ and $g\c Y\to Z$, we have $\Dom((g+1)\comp f)=\Dom(f)$ that we have already used multiple times in the concrete proofs.
\begin{lemma}
Assuming that $(X_Y,f_Y,i)$ and $(X_Y,p,i)$ are pullbacks in the following diagram, then $p=g\comp f_Y$.
\begin{equation*}
\begin{tikzcd}[ampersand replacement=\&]
{X_Y} \& X \\
Y \& {Y+Q} \\
Z \& {Z+Q'}
\arrow["i", tail, from=1-1, to=1-2]
\arrow["{f_Y}"', from=1-1, to=2-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\arrow["p"', bend right=50, from=1-1, to=3-1]
\arrow["f", from=1-2, to=2-2]
\arrow["{\inl_Y}"', tail, from=2-1, to=2-2]
\arrow["{g}"', from=2-1, to=3-1]
\arrow["g+q", from=2-2, to=3-2]
\arrow["{\inl_Z}"', tail, from=3-1, to=3-2]
\end{tikzcd}
\end{equation*}
\end{lemma}
\begin{proof}
IT simply relies on the fact that injections in an extensive category are assumed to be monic, and that the pullback of a monomorphism gives a monomorphism leg in the pullback's span.
\end{proof}
Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g\rightarrowtail X$, and $X_f$ and $X_g$ are pullbacks of $f$ and $\inl$, and $g$ and $\inl$ accordingly, then $f\appr g$ if there exists $h\c X_f\rightarrowtail X_g$ that commutes in the following diagram: Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g\rightarrowtail X$, and $X_f$ and $X_g$ are pullbacks of $f$ and $\inl$, and $g$ and $\inl$ accordingly, then $f\appr g$ if there exists $h\c X_f\rightarrowtail X_g$ that commutes in the following diagram:
\begin{equation*} \begin{equation*}
\begin{tikzcd}[ampersand replacement=\&] \begin{tikzcd}[ampersand replacement=\&]
@@ -2335,50 +2523,82 @@ Assuming $f,g\in\Hom(X,Y+1)$, and that $f'\c X_f\rightarrowtail X$ and $g'\c X_g
The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order. The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.
\end{lemma} \end{lemma}
\begin{proof} \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 Fg\comp k$ that means we have two cases: \begin{equation*}
\begin{itemize} \begin{tikzcd}[ampersand replacement=\&]
\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$. \& Z \& \\
\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed {X_h} \&\& {Z+1} \\
\end{itemize} {X_k} \& X \\
Y \& {Y+1} \\
Z \& {Z+1}
\arrow["{\inl_Z}", tail, from=1-2, to=2-3]
\arrow["q", from=2-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=2-1, to=2-3]
\arrow["e"', dashed, from=2-1, to=3-1]
\arrow["{h_d}", tail, from=2-1, to=3-2]
\arrow["{k_d}", tail, from=3-1, to=3-2]
\arrow["{k_Y}"', from=3-1, to=4-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-1, to=4-2]
\arrow["p"', bend right=50, from=3-1, to=5-1]
\arrow["h"', from=3-2, to=2-3]
\arrow["k"', from=3-2, to=4-2]
\arrow["{\inl_Y}"', tail, from=4-1, to=4-2]
\arrow["g"', from=4-1, to=5-1]
\arrow["{g+1}"', from=4-2, to=5-2]
\arrow["{\inl_Z}"', tail, from=5-1, to=5-2]
\end{tikzcd}
\end{equation*}
We define $k'=k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}$. We have:
\begin{align*}
(g+1)\comp k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}\\
(g+1)\comp k\comp\mathsf{iso}\comp(h_d+1)\comp\mathsf{iso}
\end{align*}
\todo{Finish! Perhaps, $k'=k\comp\mathsf{iso}\comp(k_d+1)\comp(e+1)\comp\mathsf{iso}$.}
\end{proof} \end{proof}
To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. We take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist: %\begin{proof}
\begin{equation*} % For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr Fg\comp k$ that means we have two cases:
\begin{tikzcd}[ampersand replacement=\&] % \begin{itemize}
{R_{X^2}} \& R \& {R_{2\times X}} \& R \\ % \item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$.
{X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\ % \item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
\& {R_1} \& R \\ % \end{itemize}
\& 1 \& {X^2+(2\times X)+1} %\end{proof}
\arrow["{q_1}", from=1-1, to=1-2] %To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. We take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
\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{equation*}
% \begin{tikzcd}[ampersand replacement=\&] % \begin{tikzcd}[ampersand replacement=\&]
% R \& I \& {X^2+(2\times X)+1} % {R_{X^2}} \& R \& {R_{2\times X}} \& R \\
% \arrow["e", two heads, from=1-1, to=1-2] % {X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3] % \& {R_1} \& R \\
% \arrow["m", tail, from=1-2, to=1-3] % \& 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{tikzcd}
%\end{equation*} %\end{equation*}
So, we have the following: %%\begin{equation*}
\begin{gather*} %% \begin{tikzcd}[ampersand replacement=\&]
R\iso R_{X^2}+R_{2\times X}+R_{1} %% R \& I \& {X^2+(2\times X)+1}
\end{gather*} %% \arrow["e", two heads, from=1-1, to=1-2]
And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$. %% \arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3]
\sgnote{This abstraction is unfinished: the crux $R_{2\times X}\iso 0$ (the ``no mixed pairs'' content of \autoref{lem:maybe-func-set}) is stated but not proved, and the subsection ends here. Either complete the argument or mark it clearly as work in progress.} %% \arrow["m", tail, from=1-2, to=1-3]
%% \end{tikzcd}
%%\end{equation*}
%So, we have the following:
%\begin{gather*}
% R\iso R_{X^2}+R_{2\times X}+R_{1}
%\end{gather*}
%And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$.
%\sgnote{This abstraction is unfinished: the crux $R_{2\times X}\iso 0$ (the ``no mixed pairs'' content of \autoref{lem:maybe-func-set}) is stated but not proved, and the subsection ends here. Either complete the argument or mark it clearly as work in progress.}
\section{Relators} \section{Relators}
\subsection{Two-way similarity in Hughes-Jacobs} \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: 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:
@@ -2874,65 +3094,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
% \end{enumerate} % \end{enumerate}
%\end{definition} %\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'$.
\end{definition}
\begin{definition}[Coliftable Order Structure]\label{def:coliftable-ord}
A \emph{coliftable 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$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, and $g$ is surjective, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}
\begin{lemma}\label{lem:set-ord-str}
In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure.
\end{lemma}
\begin{proof}
For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$.
Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$.
Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$.
\qed
\end{proof}
\begin{remark}\label{rem:set-ord-str-co}
The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
\end{remark}
\begin{lemma}\label{lem:liftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, then for every $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
\end{proof}
\begin{lemma}\label{lem:coliftable}
Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $f\in\Hom(X,FY)$ we have:
\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
\end{enumerate}
\end{lemma}
\begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\appr)} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is coliftable, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{(\appr\comp Ff)} x$.
Assuming $t\mathrel{(\appr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:coliftable-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*}
(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
\end{gather*}
So it follows directly from applying $\op$ on both sides of $(I)$.\qed
\end{proof}
%\begin{prop} %\begin{prop}
% For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a coliftable order structure $\appr$, the following propositions hold: % For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a coliftable order structure $\appr$, the following propositions hold:
% \begin{enumerate} % \begin{enumerate}
@@ -2976,40 +3138,14 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\begin{proof} \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 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} \end{proof}
\begin{example} %\begin{example}
In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$. % In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$.
%
Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$. % Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$.
%
Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf g(k')$.\qed % Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means $z\in\powf g(k')$.\qed
\end{example} %\end{example}
The following example justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective:
\begin{example}
If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is NOT an example of a coliftable order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$,
\begin{gather*}
g(z)=
\begin{cases}
0 & z\in\mathbb{Z}^+ \\
1 & \mathsf{otherwise}
\end{cases}
\end{gather*}
then
\begin{gather*}
\powf g(A)=
\begin{cases}
\emptyset & A=\emptyset \\
\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\
\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
\{0,1\} & \mathsf{otherwise}
\end{cases}
\end{gather*}
then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
\end{example}
\begin{example}
In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$.
Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed
\end{example}
\begin{definition}[Natural Relator] \begin{definition}[Natural Relator]
An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$. An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$.
\end{definition} \end{definition}
@@ -3101,7 +3237,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
\begin{proof} \begin{proof}
\todo{Finish.} \todo{Finish.}
\end{proof} \end{proof}
\subsection{Symmetrization of a Barr relator} \subsection{Symmetrization of a lax Barr relator}
\begin{prop} \begin{prop}
Assuming $F$ is the maybe functor $FX=X+1$, then the syemmetrization of the left-lax Barr relator of $F$ is a Barr-relator. Assuming $F$ is the maybe functor $FX=X+1$, then the syemmetrization of the left-lax Barr relator of $F$ is a Barr-relator.
\end{prop} \end{prop}