minor

draft/draft.tex

@@ -293,6 +293,7 @@
 \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{\sappr}{\sqsupseteq}
+\newcommand{\Dom}{\mathsf{Dom}}
 
 \newcommand{\simeet}{%
 	\mathbin{%
@@ -2192,18 +2193,18 @@ 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 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)$ ($\Dom(f)$ is the domain of a function $f$). 
 Now, we prove that the given order on the maybe functor is a liftable one.
 \begin{lemma}\label{lem:maybe-lif}
 	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 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}
-		\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}
+%	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}
+%		\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$
 \end{proof}
 \begin{lemma}\label{lem:maybe-colif}
 	The order structure on the set-functor $FX=X+1$ is a coliftable order.
@@ -2293,28 +2294,28 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
 \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},\\
+		\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)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3},
+		\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:
+	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 $Fp_2\comp\sigma(x_1,x_2)=\bot$: In this case, we have
+		\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,&\\
+			(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&(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&(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&(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).
+			\Rightarrow&\alpha(x_2)=(p_1+1)\comp\sigma(x_1,x_2).
 		\end{align*}
 	\end{itemize}\qed
 \end{proof}
@@ -3101,7 +3102,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-\subsection{Symmetrization of a Barr relator}
+\subsection{Symmetrization of a lax Barr relator}
 \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}