one-sided barr relator

draft/draft.tex

@@ -291,6 +291,7 @@
 \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{%
@@ -2209,6 +2210,38 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\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}