The concrete proof for maybe revisited

draft/draft.tex

@@ -2206,7 +2206,7 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 	\end{itemize}
 \end{proof}
 \begin{lemma}\label{lem:maybe-colif}
-	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 coliftable 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 $Fg(k)\appr h$, 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:
@@ -2217,64 +2217,106 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 	\end{itemize}
 \end{proof}
 So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$.
-\begin{lemma}\label{lem:maybe-func-set}
+%\begin{lemma}\label{lem:maybe-func-set}
-	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ 
+%	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ 
-	\begin{gather*}
-		\alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\
-		\alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot
-	\end{gather*} 
-\end{lemma}
-\begin{proof}
-	By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}:
-	\begin{enumerate}
-		\item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
-		\item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
-		\item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}
-		\item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4}
-	\end{enumerate}
-	Now, we have two cases:
-	\begin{itemize}
-		\item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $Fp_1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $Fp_2\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$.
-		\item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $Fp_2\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $Fp_1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed
-	\end{itemize}
-\end{proof}
-%\begin{proof}
-%	We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have 
 %	\begin{gather*}
-%		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot,
+%		\alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\
+%		\alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot
+%	\end{gather*} 
+%\end{lemma}
+%\begin{proof}
+%	By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. %Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}:
+%%	\begin{enumerate}
+%%		\item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
+%%		\item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
+%%		\item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}
+%%		\item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4}
+%%	\end{enumerate}
+%	For every $(x_1,x_2)$ we have
+%	\begin{enumerate}
+%		\item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
+%		\item $\alpha(x_2)\sappr Fp_2\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)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
+%		\item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
+%	\end{enumerate}
+%	Now, we have two cases:
+%	\begin{itemize}
+%		\item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $Fp_1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $Fp_2\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$.
+%		\item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $Fp_2\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $Fp_1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed
+%	\end{itemize}
+%\end{proof}
+%%\begin{proof}
+%%	We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have 
+%%	\begin{gather*}
+%%		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot,
+%%	\end{gather*}
+%%	or
+%%	\begin{gather*}
+%%		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X.
+%%	\end{gather*}
+%%	Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark
+%%	
+%%	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while  $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
+%%\end{proof}
+%
+%\begin{prop}\label{prop:sym-sim-bis-maybe}
+%	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}
+%	By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either have 
+%	\begin{gather*}
+%		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot,
 %	\end{gather*}
 %	or
 %	\begin{gather*}
-%		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X.
+%		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X.
 %	\end{gather*}
-%	Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark
+%	We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows:
-%	
+%	\begin{gather*}
-%	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while  $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
+%		\beta(x_1,x_2)=
+%		\begin{cases} 
+%			\bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot  \\
+%			(\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 $Fp_i\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $Fp_i\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 $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}
 
-\begin{prop}\label{prop:sym-sim-bis-maybe}
+\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}
-	By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either 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{gather*}
+	\begin{enumerate}
-		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot,
+		\item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1},
-	\end{gather*}
+		\item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\
-	or
+		%	\end{enumerate}
-	\begin{gather*}
+	and since $R$ is symmetric, we have 
-		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X.
+	%		\begin{enumerate}
-	\end{gather*}
+		\item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2},
-	We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows:
+		\item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
-	\begin{gather*}
+	\end{enumerate}
-		\beta(x_1,x_2)=
+	Followed by $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$ we have the following cases:
-		\begin{cases} 
+	\begin{itemize}
-			\bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot  \\
+		\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.
-			(\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X
+		\item $Fp_2\comp\sigma(x_1,x_2)=\bot$: In this case, we have
-		\end{cases}
+		\begin{align*}
-	\end{gather*}
+			p_2+1\comp\sigma(x_1,x_2)=\bot,&\\
-	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $Fp_i\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.
+			\Rightarrow&\sigma(x_1,x_2)=\bot,\\
-	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$.
+			\Rightarrow&p_1+1\comp\sigma(x_1,x_2)=\bot,\\
-	\qed
+			\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)\bot.
+		\end{align*}
+	\end{itemize}\qed
 \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.}
@@ -3049,9 +3091,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-\begin{lemma}
+\subsection{Symmetrization of a Barr relator}
-	The non-trivial order on the maybe functor $FX=X+1$ is a liftable order.
-\end{lemma}
 \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.
 \end{prop}
@@ -3073,6 +3113,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{remark}
 	With a similar argument we can prove that the symmetrization of a right-lax Barr-relator of $F$ is a Barr-relator.
 \end{remark}
+\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion.}
 \end{document}