more props added

draft/draft.tex

@@ -288,6 +288,7 @@
 \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}}
 
@@ -2149,16 +2150,37 @@ 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}
+\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:
+	\todo{Finish.}
-	\begin{itemize}
+\end{proof}
-		\item ${\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$, or $({\relar}(f^\op\comp g))^\op\leq(Fg)^\op\comp Ff$
+The symmetrization of the Egli-Milner relator is a Barr-relator. Barr-relators is a generalization of the Egli-Milner relator, where the functor is generalized.
-		\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}
+\begin{prop}
-	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.
+	Assuming that $r\c X\rto Y$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then $\appr_{X};\hat{\emre};\appr_{Y}=\appr_{X};\hat{\emre}$ and $\appr_{X};\hat{\emre}=\hat{\emre};\appr_{Y}$.
+\end{prop}
+
+\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}
+	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}