pc sync

draft/.gitignore

@@ -20,7 +20,7 @@
 # these rules might exclude image files for figures etc.
 # *.ps
 # *.eps
-# *.pdf
+*.pdf
 
 ## Generated if empty string is given at "Please type another file name for output:"
 .pdf

draft/draft.tex

@@ -288,8 +288,10 @@
 \newcommand{\gra}{\mathbf{Gra}}
 \newcommand{\obj}{\mathbf{Obj}}
 \newcommand{\relar}{\mathbf{R}}
+\newcommand{\emre}{\mathbf{L}}
 \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
 \newcommand{\powf}{\mathcal{P}}
+\newcommand{\sappr}{\sqsupseteq}
 
 \newcommand{\simeet}{%
 	\mathbin{%
@@ -2149,16 +2151,102 @@ then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in
 \begin{cor}
 	Assuming that a relator $\relar$ over a functor $F\c\Set\to\Set$ satisfies $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$ for every functions $f\c X\to Z$ and $g\c Y\to Z$, then $\hat{\relar}$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete, using the axiom of choice.
 \end{cor}
+\subsection{Egli-Milner relator and Barr relators}
+\begin{definition}
+	We call the map $\emre\c\rel\to\rel$ the Egli-Milner $\powf$-relator, whenever for every relation $r\c X\rto Y$ it is defined as follows:
+	\begin{gather*}
+		\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
+	\end{gather*}
+\end{definition}
+Egli-Milner relator is not sound or complete, although its symmetrization is sound and complete.
 \begin{prop}
-	Assuming that for a relator $\relar$ over $F\c\Set\to\Set$, $\hat{\relar}$ is difunctionally functorial, then $\relar$ is also difunctionally functorial, and vice-versa.
+	$\hat{\emre}$-similarity from a coalgebra $(\alpha,X)$ to $(\beta,Y)$ is sound and complete.
 \end{prop}
 \begin{proof}
-	$\hat{\relar}$ being difunctionally functorial means that for every functions $f\c X\to FX$ and $g\c Y\to FY$, we have $\hat{\relar}(g^\op\comp f)=(Fg)^\op\comp Ff$. It is equivalent with the both following conditions being true:
-	\begin{itemize}
-		\item ${\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$, or $({\relar}(f^\op\comp g))^\op\leq(Fg)^\op\comp Ff$
-		\item ${\relar}(g^\op\comp f)\geq(Fg)^\op\comp Ff$ and $({\relar}(f^\op\comp g))^\op\geq(Fg)^\op\comp Ff$
-	\end{itemize}
-	The proof from right to left is obvious. For the other direction we assume that $\hat{\relar}$ is difunctinally functorial. Then we have $\hat{\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$ and $\hat{\relar}(g^\op\comp f)\geq(Fg)^\op\comp Ff$. The earlier gives the first item, and the later gives the second item.
+	We need to prove that for every functions $f\c X\to Z$ and $g\c Y\to Z$, $\hat{\emre}(g^\op\comp f)=(\powf g)^\op\comp\powf f$. 
+	We have $S\;\hat{\emre}(g^\op\comp f)\;T$ iff $S\;\emre(g^\op\comp f)\;T$ and $T\;\emre(f^\op\comp g)\;S$. Then we have
+	\begin{align*}
+		S\;\emre(g^\op\comp f)\;T&\\
+		&\iff\forall x\in S,\exists y\in T, x\;g^\op\comp f\; y\\
+		&\iff \forall x\in S,\exists y\in T,z\in Z, x\;f\;z\; , \; y\;g\;z,
+	\end{align*}
+	and
+	\begin{align*}
+		T\;\emre(f^\op\comp g)\;S&\\
+		&\iff\forall y\in T,\exists x\in S, y\;f^\op\comp g\; x\\
+		&\iff \forall y\in T,\exists x\in S, z\in Z, x\;f\;z\; , \; y\;g\;z.
+	\end{align*}
+	It is equivalent with the following:
+	\begin{gather*}
+		\forall x\in S,\exists y\in T, f(x)=g(y),\\
+		\forall y\in T,\exists x\in S, f(x)=g(y).
+	\end{gather*}
+	Equivalently, $Im(f\mid_S)=Im(g\mid_T)$, and we call images $U$ that is in $\powf Z$. So, we equivalently have
+	\begin{align*}
+		S\;\powf f\;U,\; T\;\powf g\;U&\\
+		&\iff S\;\powf f\;U,\; U\;(\powf g)^\op\;T\\
+		&\iff S\;(\powf g)^\op\comp\powf f\;T
+	\end{align*}\qed
+\end{proof}
+For every relation $r\rto X\to Y$ $\emre r=\subseteq\;\emre r=\emre r\;\subseteq=\subseteq;\emre r;\subseteq$.
+%\begin{prop}
+%	Assuming that $r\c X\rto Y$, then $\subseteq;\hat{\emre}r;\subseteq=\subseteq;\hat{\emre}r$ and $\subseteq;\hat{\emre}r=\hat{\emre}r;\subseteq$.
+%\end{prop}
+
+
+Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.
+
+\begin{definition}
+	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}
+	$\hat{L}$ is a Barr relator.
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+
+\begin{definition}[One-sided Barr relator]
+	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
+	\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.
+\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:
+	\begin{align*}
+		s \;\hat{\overrightarrow{F}}r\; 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\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
+	\end{align*}
+	Since $F\pi_1$ is a function, then $(F\pi_1)^\op$ is an injective map, so there exist exactly one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
+	\begin{gather*}
+		w\;F\pi_2\comp\sappr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
+	\end{gather*}
+	And similarly, since $F\pi_2$ is also a function we have exactly one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
+	\begin{align*}
+		&w\;\sappr\; 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)\;=\; (F\pi_2^\op)(t)\\
+		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
+		\iff&s\;\bar{F}r\;t
+	\end{align*}\qed
+\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.
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
 \end{proof}
 \end{document}