no maybe anymore

draft/draft.tex

@@ -2193,8 +2193,8 @@ Now, we prove our main statement.
 \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.
 \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 sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$ ($\Dom(f)$ is the domain of a function $f$). 
+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}
 	The order structure on the set-functor $FX=X+1$ is a liftable order.
 \end{lemma}
@@ -2204,7 +2204,15 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 %		\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
 %	\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$
+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}
 \begin{lemma}\label{lem:maybe-colif}
 	The order structure on the set-functor $FX=X+1$ is a coliftable order.
@@ -2287,41 +2295,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$.
 %	\qed
 %\end{proof}
-
+%%%%%%Second proof:
 \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.
 \end{prop}
 \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
-	\begin{enumerate}
-		\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},\\
-		%	\end{enumerate}
-	and since $R$ is symmetric, we have 
 %	\begin{enumerate}
-		\item $\alpha(x_2)=(p_1+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
+%		\item $\alpha(x_1)=(p_1+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
-		\item $\alpha(x_1)\sappr (p_2+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
+%		\item $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
+%		%	\end{enumerate}
+%	and since $R$ is symmetric, we have 
+%	%		\begin{enumerate}
+%		\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},
+%	\end{enumerate}
+%	Followed by $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$ we have the following cases:
+%	\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 $p_2+1\comp\sigma(x_1,x_2)=\bot$: In this case, we have
+%		\begin{align*}
+%			(p_2+1)\comp\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&\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&\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)=(p_1+1)\comp\sigma(x_1,x_2).
+%		\end{align*}
+%	\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 $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$ we have the following cases:
+	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{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 $p_2+1\comp\sigma(x_1,x_2)=\bot$: In this case, we have
 	\begin{align*}
-			(p_2+1)\comp\sigma(x_1,x_2)=\bot,&\\
+		\Dom((p_2+1)\comp\sigma)&\\
-			\Rightarrow&\sigma(x_1,x_2)=\bot,\\
+		=&\Dom(\sigma)\\
-			\Rightarrow&(p_1+1)\comp\sigma(x_1,x_2)=\bot,\\
+		=&\Dom((p_1+1)\comp\sigma)\\
-			\Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\
+		=&\Dom(\alpha\comp p_1)&\by{\eqref{eq:maybe-func-set-1}}\\
-			\Rightarrow&(p_2+1)\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\
+		=&\Dom(\alpha\comp p_1\comp s)\\
-			\Rightarrow&\sigma(x_2,x_1)=\bot,\\
+		=&\Dom(\alpha\comp p_2)
-			\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)=(p_1+1)\comp\sigma(x_1,x_2).
 	\end{align*}
-	\end{itemize}\qed
+	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}
 
-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.
+ 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:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
@@ -2336,50 +2382,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.
 \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 Fg\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 $Fg\comp k'=h$.
-		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
-	\end{itemize}
-\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{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
-		{R_{X^2}} \& R \& {R_{2\times X}} \& R \\
+			\& Z \& \\
-		{X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
+			{X_h} \&\& {Z+1} \\
-		\& {R_1} \& R \\
+			{X_k} \& X \\
-		\& 1 \& {X^2+(2\times X)+1}
+			Y \& {Y+1} \\
-		\arrow["{q_1}", from=1-1, to=1-2]
+			Z \& {Z+1}
-		\arrow["{q_2}"', from=1-1, to=2-1]
+			\arrow["{\inl_Z}", tail, from=1-2, to=2-3]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
+			\arrow["q", from=2-1, to=1-2]
-		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-2, to=2-2]
+			\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=2-1, to=2-3]
-		\arrow["{r_1}", from=1-3, to=1-4]
+			\arrow["e"', dashed, from=2-1, to=3-1]
-		\arrow["{r_2}"', from=1-3, to=2-3]
+			\arrow["{h_d}", tail, from=2-1, to=3-2]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4]
+			\arrow["{k_d}", tail, from=3-1, to=3-2]
-		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-4, to=2-4]
+			\arrow["{k_Y}"', from=3-1, to=4-1]
-		\arrow["{\mathsf{in}_1}"', from=2-1, to=2-2]
+			\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-1, to=4-2]
-		\arrow["{\mathsf{in}_2}"', from=2-3, to=2-4]
+			\arrow["p"', bend right=50, from=3-1, to=5-1]
-		\arrow["{s_1}", from=3-2, to=3-3]
+			\arrow["h"', from=3-2, to=2-3]
-		\arrow["{s_2}"', from=3-2, to=4-2]
+			\arrow["k"', from=3-2, to=4-2]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3]
+			\arrow["{\inl_Y}"', tail, from=4-1, to=4-2]
-		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=3-3, to=4-3]
+			\arrow["g"', from=4-1, to=5-1]
-		\arrow["{\mathsf{in}_3}"', from=4-2, to=4-3]
+			\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}
+%\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{itemize}
+%		\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$.
+%		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
+%	\end{itemize}
+%\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{equation*}
 %	\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{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}
 \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: