the equality

draft/draft.tex

@@ -2334,7 +2334,26 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{definition}[Cogood Order Structure]\label{def:cogood-ord}
 	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}
+\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{lemma}
+\begin{proof}
+	$(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 $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$.
+	
+	$(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{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$
@@ -2342,11 +2361,16 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\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 good, 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$.
+	$(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)$\todo{Finish.}
+	$(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:
@@ -2375,34 +2399,21 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	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{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.