Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

ACV-abstract-2026/sym-sim.tex

@@ -241,7 +241,7 @@ We ask:
 \begin{enumerate}
   \item How to construct relators for established notions of simulation? 
   \item How to generally prove that ensuing symmetric simulations are bisimulations?
-  \item How alternative notions of simulations align with the relator-based one? 
+  \item How alternative notions of simulation align with the relator-based one? 
 \end{enumerate}
 
 \paragraph{Relaxing Barr Relators} %\label{sec:} 

draft/draft.tex

@@ -2321,68 +2321,135 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-\begin{definition}[Cogood Order Structure]\label{def:cogood}
+\begin{definition}[Natural Order Structure]\label{def:nat-ord}
-	A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that:
+	A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X\to X'$, $g\c Y\to Y'$, then:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
-		\item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $g\c Y\to Y'$, then $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$.\label{item:cogood:I}
+		\item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',Y)$. \label{item:nat-ord:I}
-		\item If $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\label{item:cogood:II}
+		\item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$. \label{item:nat-ord:II}
 	\end{enumerate}
 \end{definition}
-\begin{prop}
+\begin{definition}[Good Order Structure]\label{def:good-ord}
-	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
+	A \emph{good order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr  Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
-	\begin{enumerate}
+\end{definition}
-		\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
+\begin{definition}[Cogood Order Structure]\label{def:cogood-ord}
-		\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
+	A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
+\end{definition}
+
+\begin{lemma}\label{lem:good}
+	Assuming that a a functor $F$ has an order structure $\appr$ that is good, then for every $f\in\Hom(X,FY)$ we have:
+	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
+		\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
+		\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
 	\end{enumerate}
-\end{prop}
+\end{lemma}
 \begin{proof}
-	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$.
+	$(I)$ Assuming $t\mathrel{Ff\comp\sappr} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is good, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{\sappr\comp Ff} x$.
 	
-	Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
+	Assuming $t\mathrel{\sappr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:good-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$.
-	\begin{gather*}
-		z \mathrel{(F\pi_i)} x,\\
-		z \mathrel{\appr} z',\\
-		z'\mathrel{(F\pi_j)} y.
-	\end{gather*}
-	Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
 	
-	Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
+	$(II)$ Basically, by definition of $\op$ and relation composition we have
 	\begin{gather*}
-		z\mathrel{(F\pi_i)} x,\\
+		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
-		z \mathrel{(F\pi_j)} y',\\
+		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
-		y' \mathrel{\appr} y.
 	\end{gather*}
-	Since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:II} there exists a $w$ such that  $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$,  $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed
+	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
 \end{proof}
+\begin{lemma}\label{lem:cogood}
+	Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, then for every $f\in\Hom(X,FY)$ we have:
+	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
+		\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
+		\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
+	\end{enumerate}
+\end{lemma}
+\begin{proof}
+	$(I)$ Assuming $t\mathrel{Ff\comp\appr} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is cogood, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{\appr\comp Ff} x$.
+	
+	Assuming $t\mathrel{\appr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:cogood-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$.
+	
+	$(II)$ Basically, by definition of $\op$ and relation composition we have
+	\begin{gather*}
+		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
+		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
+	\end{gather*}
+	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
+\end{proof}
+%\begin{prop}
+%	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
+%	\begin{enumerate}
+%		\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
+%		\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
+%	\end{enumerate}
+%\end{prop}
+%\begin{proof}
+%	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$.
+%	
+%	Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
+%	\begin{gather*}
+%		z \mathrel{(F\pi_i)} x,\\
+%		z \mathrel{\appr} z',\\
+%		z'\mathrel{(F\pi_j)} y.
+%	\end{gather*}
+%	Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
+%	
+%	Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
+%	\begin{gather*}
+%		z\mathrel{(F\pi_i)} x,\\
+%		z \mathrel{(F\pi_j)} y',\\
+%		y' \mathrel{\appr} y.
+%	\end{gather*}
+%	Since $\appr$ is a cogood order structure by~\autoref{def:cogood-ord} there exists a $w$ such that  $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$,  $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed
+%\end{proof}
 \begin{prop}
-	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
+	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has an order structure $\appr$, the following propositions hold:
 	\begin{enumerate}
-		\item $F\pi_2\comp\sappr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$
+		\item If $\appr$ is good, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$
-		\item $F\pi_1\comp\sappr\comp(F\pi_2)^\op\quad=\quad F\pi_1\comp(F\pi_2)^\op\comp\appr$
+		\item If $\appr$ is cogood, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$
+		\item If $\appr$ is both good and cogood, all the following are equal:
+		\begin{itemize}
+			\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad$
+			\item $F\pi_2\comp(F\pi_1)^\op\comp\appr$
+			\item $\appr\comp F\pi_2\comp(F\pi_1)^\op$
+			\item $\appr\comp F\pi_2\comp(F\pi_1)^\op\comp\appr$
+		\end{itemize}
 	\end{enumerate}
 \end{prop}
 \begin{proof}
-	\todo{Finish.}
+	They all follow in an obvious way from~\autoref{lem:good} and~\autoref{lem:cogood}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
 \end{proof}
+\begin{example}
+	In the category of sets, subset over the powerset functor is an example of a good order. For every $h\c X\to\powf Z$, $k\c X\to \powf Y$, and $g\c Y\to Z$, such that $h\subseteq\powf g\comp k$, there exists $k'\c X\to\powf Y$ that for every $x\in X$, $k'(x)=k(x)\setminus\{y\mid g(y)\notin h(x)\}$. We show that for every $x\in X$, we have $\powf g\comp k'(x)=h(x)$.
+	
+	Assuming $z\in\powf g(k'(x))$, then there exist $y'\in k(x)\setminus \{y\mid g(y)\notin h(x)\}$ that $g(y')=z$, so $y'\in k(x)$, $y'\notin\{y\mid g(y)\notin h(x)\}$. $y'\notin\{y\mid g(y)\notin h(x)\}$ means that $g(y')\in h(x)$, thus $\powf g\comp k'\subseteq h$.
+	
+	Assuming $z\in h(x)$, since $h\subseteq \powf g\comp k$, then $z\in\powf g\comp k(x)$. So, there exists $y'$ such that $y'\in k(x)$ and $g(y')=z$. Since $g(y')\in h(x)$ then $y'\notin\{y\mid g(y)\notin h(x)\}$ meaning that $y'\in k'(x)$ that means $z\in \powf g(k'(x))$, thus $h\subseteq \powf g\comp k'$.\qed
+\end{example}
+\begin{example}
+	In the category of sets, subset over the powerset functor is NOT an example of a cogood order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, 
+	\begin{gather*}
+		g(z)=
+		\begin{cases} 
+			0 & z\in\mathbb{Z}^+ \\
+			1 & \mathsf{otherwise}  
+		\end{cases}
+	\end{gather*}
+	then 
+	\begin{gather*}
+		\powf g(A)=
+		\begin{cases} 
+			\emptyset & A=\emptyset \\
+			\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\  
+			\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
+			\{0,1\} & \mathsf{otherwise} 
+		\end{cases}
+	\end{gather*}
+	then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
+\end{example}
+The previous example suggests that cogoodness is a strong condition. Perhaps it can be limited to be meaningful. Maybe the morphism $g$ can be limited to legs of a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, where for a relation $r$, $r=\pi_2\comp\pi_1^\op$.
 \begin{prop}
-	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
+	For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is cogood.
-	\begin{enumerate}
-		\item $F\pi_2\comp\appr\comp\sappr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op\comp\appr$
-		\item $F\pi_1\comp\appr\comp\sappr\comp(F\pi_2)^\op\quad=\quad \appr\comp F\pi_1\comp(F\pi_2)^\op\comp\appr$
-	\end{enumerate}
 \end{prop}
 \begin{proof}
-	\todo{Finish.}
+	\todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a good order structure forces every witness for AM-simulation to have the left cell of the lax diagram as equality, and subset on powerset functor is a good order structure, then what is the counter-example number 4 that you have?!}
-\end{proof}
-\begin{prop}
-	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a good order structure $\appr$, the following propositions hold:
-	\begin{enumerate}
-		\item $F\pi_2\comp\sappr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
-		\item $F\pi_1\comp\sappr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
-	\end{enumerate}
-\end{prop}
-\begin{proof}
-	\todo{Finish.}
 \end{proof}
 \begin{prop}
 	Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator. 
@@ -2396,7 +2463,6 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-
 \end{document}