doesn't seem to work!

draft/draft.tex

@@ -2269,10 +2269,10 @@ So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra
 	\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$.
+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$.
 %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$.}
+	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 g+1\comp k$ that means we have two cases:
@@ -2281,11 +2281,12 @@ Now, we want to abstract the given proof for an arbitrary category that has copr
 		\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}
+To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category 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$. In our case, 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=\&]
-		{I_{X^2}} \& R \& {I_{(2\times X)}} \& R \\
+		{R_{X^2}} \& R \& {R_{2\times X}} \& R \\
 		{X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
-		\& {I_1} \& R \\
+		\& {R_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]
@@ -2304,17 +2305,19 @@ Now, we want to abstract the given proof for an arbitrary category that has copr
 		\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{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*}
+So, we have the following:
 \begin{gather*}
-	I\iso I_{X^2}+I_{2\times X}+I_{1}
+	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$. 
 \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: