Egli-Milner proof

draft/draft.tex

@@ -2162,9 +2162,32 @@ Egli-Milner relator is not sound or complete, although its symmetrization is sou
 	$\hat{\emre}$-similarity from a coalgebra $(\alpha,X)$ to $(\beta,Y)$ is sound and complete.
 \end{prop}
 \begin{proof}
-	\todo{Finish.}
+	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)=Im(g)$, 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}
-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.
+The symmetrization of the Egli-Milner relator is a Barr-relator. Barr-relator is a generalization of the Egli-Milner relator, where the functor is generalized.
 
 \begin{prop}
 	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}$.