sound and complete!

draft/draft.tex

@@ -2468,6 +2468,16 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b
 \begin{definition}[Natural Relator]
 	An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$.
 \end{definition}
+\begin{definition}[Relaional Connector]
+	A natural $F$-relator $\relar$ is a \emph{relational connector}, whenever for every set $X$, $\id_{FX}\subseteq\relar\id_X$.
+\end{definition}
+\begin{definition}[Normal Relator]
+	An $F$-relator $\relar$ is \emph{normal}, whenever for every set $X$, $\id_{FX}=\relar\id_X$.
+\end{definition}
+\begin{prop}
+	Every normal relational connect is difunctionally functorial.\qed
+\end{prop}
+
 \begin{prop}
 	Assuming that a set-functor $F$ has a good order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. 
 \end{prop}
@@ -2475,17 +2485,59 @@ The following example justifies why the $g$ in~\autoref{def:cogood-ord} should b
 	\begin{align*}
 		\relar (g^\op\comp r\comp f)&\\
 		=&\appr\comp F(g^\op\comp r\comp f)\\
-		=&\appr\comp(Fg^\op)\comp F(r)\comp F(f)\\
+		=&\appr\comp(Fg^\op)\comp Fr\comp Ff\\
-		=&(Fg^\op)\comp\appr\comp F(r)\comp F(f)\\
+		=&(Fg^\op)\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:good}}\\
-		=&(Fg^\op)\comp\relar r\comp F(f)
+		=&(Fg^\op)\comp\relar r\comp Ff
+	\end{align*}\qed
+\end{proof}
+\begin{remark}
+	One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is cogood. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:cogood-ord} prevents the same reasoning.
+\end{remark}
+\begin{prop}
+	Symmetrization of a natural relator, is natural.
+\end{prop}
+\begin{proof}
+	Assuming $\relar$ is a natural $F$-relator, we prove that $\hat{\relar}$ is natural as well. Assuming $r\c X\rto Y$, $f\c A\to X$, and $g\c B\to Y$, by naturality of $\relar$ we have $\relar (g^\op\comp r\comp f)=Fg^\op\comp \relar r\comp Ff$. Then we have:
+	\begin{align*}
+		\hat{\relar}(g^\op\comp r\comp f)&\\
+		=&\relar(g^\op\comp r\comp f)\cap(\relar(f^\op\comp r^\op\comp g))^\op\\
+		=&Fg^\op\comp\relar r\comp Ff\cap(Ff^\op\comp\relar r^\op\comp Fg)^\op\\
+		=&Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff
+	\end{align*}
+	So we are left to prove
+	\begin{gather*}
+		Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff=Fg^\op\comp(\relar r\cap(\relar r^\op)^\op)\comp Ff
+	\end{gather*}
+	because then we will have $\hat{\relar}(g^\op\comp r\comp f)=Fg^\op\comp\hat{\relar}\comp Ff$. We have
+	\begin{align*}
+		(t,s)\in &Fg^\op\comp\relar r\comp Ff\cap Fg^\op\comp(\relar r^\op)^\op\comp Ff,\\
+		&\iff(t,s)\in Fg^\op\comp\relar r\comp Ff\quad\&\quad (t,s)\in Fg^\op\comp(\relar r^\op)^\op\comp Ff,\\
+		&\iff Ff(t) \mathrel{(\relar r)} Fg(s) \quad\&\quad Ff(t) \mathrel{(\relar r^\op)^\op} Fg(s),\\
+		&\iff Ff(t) \mathrel{(\relar\cap(\relar r^\op)^\op)} Fg(s),\\
+		&\iff t\mathrel{(Fg^\op\comp(\relar\cap(\relar r^\op)^\op)\comp Ff)} s.
+	\end{align*}
+	It worth noting that when we have $(t,s)\in Fg^\op\comp\relar r\comp Ff$, it mean that there exist $t'$ and $s'$ that $(t,t')\in Ff$, $(t',s')\in \relar r$, and $(s',s)\in Fg^\op$. Since $Ff$ and $Fg$ are functions, then $t'=Ff(t)$ and $s'=Fg(s)$, and these are unique elements. The uniqueness enables us in the above reasoning to go from the second line to the third line.\qed 
+\end{proof}
+\begin{prop}
+	If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal.
+\end{prop}
+\begin{proof}
+	We show the left-lax Barr relator with $\relar$. We have:
+	\begin{align*}
+		\hat{\relar}\id&\\
+		=&\relar\id\cap(\relar\id^\op)^\op\\
+		=&\appr\comp F\id\cap (\appr\comp F\id^\op)^\op\\
+		=&\appr\cap\sappr\\
+		=&\id
 	\end{align*}\qed
 \end{proof}
 \begin{cor}
-	By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is good, then the mid-lax relator is natural as well.
+	Since the symmetrization of left-lax Barr relator is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
 \end{cor}
-\begin{remark}
+\begin{cor}
-	One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is cogood. But it is not the case because of the surjectivity condition on the $g$ in~\autoref{def:cogood-ord}.
+	By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is good, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well.
-\end{remark}
+\end{cor}
+Perhaps if we can relax the definition of good by allowing $g$ to be a relation rather than a function, we can have a lax Barr relator that its symmetrization is a normal lax extension.\todo{Investigate!}
 \begin{prop}
 	For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is cogood.
 \end{prop}