concrete maybe proof corrected

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'$.