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

draft/draft.tex

@@ -1025,12 +1025,12 @@ We show this relation with $F_\rel(R,X)$.
 			X \& R \& X \\
 			FX \& (FR)^\dagger \& FX
 			\arrow["\alpha"', from=1-1, to=2-1]
-			\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
+			\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
 			\arrow["{p_1}"', from=1-2, to=1-1]
 			\arrow["{p_2}", from=1-2, to=1-3]
 			\arrow["\sigma", from=1-2, to=2-2]
 			\arrow["\alpha", from=1-3, to=2-3]
-			\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
+			\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
 			\arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1]
 			\arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3]
 		\end{tikzcd}
@@ -1123,7 +1123,7 @@ We show this relation with $F_\rel(R,X)$.
 \end{proof}
 %
 Now, we give a counter example of a symmetric relation on $\Set$ that is a simulation according to~\autoref{def:sim}, i.e, exists the morphism $\sigma$ that commutes laxly in~\eqref{eq:diag-lax-sim}, but $\sigma$ is not a coalgebraic bisimulation, although the relation that we give is clearly a bisimulation in the classic sense. 
-We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\sqsubseteq=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions:
+We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\appr=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions:
 \begin{gather*}
 	A\to C_1\qquad B\to C_2\qquad C_1\to C_1\qquad C_2\to C_2\qquad C'_2\to C_2
 \end{gather*}
@@ -2194,13 +2194,28 @@ For every relation $r\rto X\to Y$ $\emre r=\subseteq\;\emre r=\emre r\;\subseteq
 
 Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.
 
-\begin{definition}
+\begin{definition}[Barr relator]
 	A relator over a functor $F$ is a Barr relator, shown by $\bar{F}$, iff for a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
 	\begin{gather*}
 		\bar{F}r=F\pi_2\comp(F\pi_1)^\op
 	\end{gather*}
 \end{definition}
-
+\begin{prop}
+	For every set-functor $F$, the barr relator $\bar{F}$ is symmetric.
+\end{prop}
+\begin{proof}
+	Assuming that for a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ we have $r=\pi_2\comp\pi_1^\op$, then we have:
+	\begin{align*}
+		\hat{\bar{F}}r&\\
+		=&\bar{F}r\cap(\bar{F}r^\op)^\op\\
+		=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_2\comp\pi_1^\op)^\op)^\op\\
+		=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_1\comp\pi_2^\op))^\op\\
+		=&F\pi_2\comp(F\pi_1)^\op\cap(F\pi_1\comp (F\pi_2)^\op)^\op\\
+		=&F\pi_2\comp(F\pi_1)^\op\cap F\pi_2\comp (F\pi_1)^\op\\
+		=&F\pi_2\comp(F\pi_1)^\op\\
+		=&\bar{F}r
+	\end{align*}\qed
+\end{proof}
 \begin{prop}
 	$\hat{L}$ is a Barr relator.
 \end{prop}
@@ -2208,66 +2223,67 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\todo{Finish.}
 \end{proof}
 
-\begin{definition}[One-sided Barr relator]
+\begin{definition}[Mid-lax Barr relator]
-	Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\sqsubseteq$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{one-sided Barr relator} iff we have:
+	Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have:
 %	A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
 	\begin{gather*}
-		\overrightarrow{F}r=F\pi_2\comp\sappr\comp(F\pi_1)^\op
+		\overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op
 	\end{gather*}
 \end{definition}
 
 \begin{prop}
-	For every functor $F\c\Set\to\Set$, the symmetrization of the one-sided Bar relator is equal with the Barr relator.
+	For every functor $F\c\Set\to\Set$, the symmetrization of the mid-lax Bar relator is equal with the Barr relator.
 \end{prop}
 \begin{proof}
-	Where there exist $\pi_1\c A\to X$ and $\pi_2\c A\to Y$ such that $r=\pi_2\comp\pi_1^\op$, we assume that $s \;\hat{\overrightarrow{F}}r\; t$, and we need to show that $s\;F\pi_2\comp(F\pi_1)^\op\;t$. Considering that $r^\op=\pi_1\comp\pi_2^\op$, we have:
+%	Where there exist $\pi_1\c A\to X$ and $\pi_2\c A\to Y$ such that $r=\pi_2\comp\pi_1^\op$, we assume that $s \;\hat{\overrightarrow{F}}r\; t$, and we need to show that $s\;F\pi_2\comp(F\pi_1)^\op\;t$. Considering that $r^\op=\pi_1\comp\pi_2^\op$, we have:
-	\begin{align*}
+%	\begin{align*}
-		s \;\hat{\overrightarrow{F}}r\; t&\\
+%		s \;\hat{\overrightarrow{F}}r\; t&\\
-		&\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\
+%		&\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\
-		&\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\sappr\comp(F\pi_2)^\op)^\op\;t\\
+%		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\
-		&\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
+%		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
-	\end{align*}
+%	\end{align*}
-	Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
+%	Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
-	\begin{gather*}
+%	\begin{gather*}
-		w\;F\pi_2\comp\sappr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
+%		w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
-	\end{gather*}
+%	\end{gather*}
-	And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
+%	And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
-	\begin{align*}
+%	\begin{align*}
-		&w\;\sappr\; v \qquad\&\qquad w\;\appr\; v\\
+%		&w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\
-		\iff&(F\pi_1)^\op(s)\;\sappr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\
+%		\iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\
-		\iff&(F\pi_1)^\op(s)\;=\; (F\pi_2^\op)(t)\\
+%		\iff&(F\pi_1)^\op(s)\;=\; (F\pi_2^\op)(t)\\
-		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
+%		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
-		\iff&s\;\bar{F}r\;t
+%		\iff&s\;\bar{F}r\;t
-	\end{align*}
+%	\end{align*}
-	So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
+%	So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
-	Now, we are left to show that $\bar{F}\leq\hat{\overrightarrow{F}}$. For that, reading the given proof from the end to the starting point is sufficient.
+%	Now, we are left to show that $\bar{F}\leq\hat{\overrightarrow{F}}$. For that, reading the given proof from the end to the starting point is sufficient.
+\todo{Finish.}
 \end{proof}
 
-\begin{lemma}
+\begin{prop}
-	The following propositions hold:
+	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ the following propositions hold:
 	\begin{enumerate}
-		\item $\powf\pi_2\comp\supseteq\comp(\powf\pi_1)^\op\quad=\quad\supseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$
+		\item $\powf\pi_2\comp\subseteq\comp(\powf\pi_1)^\op\quad=\quad\subseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$
-		\item $\powf\pi_1\comp\supseteq\comp(\powf\pi_2)^\op\quad=\quad\supseteq\comp \powf\pi_1\comp(\powf\pi_2)^\op$
+		\item $\powf\pi_1\comp\subseteq\comp(\powf\pi_2)^\op\quad=\quad\subseteq\comp \powf\pi_1\comp(\powf\pi_2)^\op$
 	\end{enumerate}
-\end{lemma}
+\end{prop}
 \begin{proof}
-	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op\quad=\quad\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$.
+	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op\quad=\quad\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$.
 	
-	Assuming $x \mathrel{\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that
+	Assuming $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that
 	\begin{gather*}
 		z \mathrel{(\powf\pi_i)} x,\\
 		z \mathrel{\subseteq} z',\\
 		z'\mathrel{(\powf\pi_j)} y.
 	\end{gather*}
-	Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\supseteq\comp \powf\pi_j} y$, thus $x\mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$.
+	Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\subseteq\comp \powf\pi_j} y$, thus $x\mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$.
 	
-	Now, assuming $x \mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
+	Now, assuming $x \mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
 	\begin{gather*}
 		z\mathrel{(\powf\pi_i)} x,\\
 		z \mathrel{(\powf\pi_j)} y',\\
 		y' \mathrel{\subseteq} y.
 	\end{gather*}
-	We take the set $w=z\cup (\powf\pi_i(z)\times y)$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$,  $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op} y$.\qed
+	We take the set $w=z\cup (\powf\pi_i(z)\times y)$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$,  $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$.\qed
 \end{proof}
 	
 %\begin{lemma}
@@ -2295,9 +2311,87 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 %		y' \mathrel{\sqsubseteq} y.
 %	\end{gather*}
 %\end{proof}
-
 \begin{prop}
-	Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
+	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is either the maybe monad, the subdistribution monad or $FX=\powf(X\times A)$, where $A$ is a set of labels, then 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}
+	\todo{Finish.}
+\end{proof}
+\begin{definition}[Cogood Order Structure]\label{def:cogood}
+	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:
+	\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 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}
+	\end{enumerate}
+\end{definition}
+\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~\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
+	\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}.\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
+\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\sappr\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$
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\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\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.}
+\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. 
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+\begin{prop}
+	Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
 \end{prop}
 \begin{proof}
 	\todo{Finish.}