order

draft/draft.tex

@@ -2319,8 +2319,18 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph
 	\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.}
+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.}
 %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.
+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=\&]
+		{X_g} \& X \\
+		{X_f}
+		\arrow["{g'}", tail, from=1-1, to=1-2]
+		\arrow["h", dashed, tail, from=2-1, to=1-1]
+		\arrow["{f'}"', tail, from=2-1, to=1-2]
+	\end{tikzcd}
+\end{equation*}
 \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.
 \end{lemma}