proof

draft/draft.tex

@@ -2209,7 +2209,8 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \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:
+	Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\sqsubseteq$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{one-sided Barr relator} iff we have:
+%	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*}
@@ -2242,19 +2243,66 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	Now, we are left to show that $\bar{F}\leq\hat{\overrightarrow{F}}$. For that, reading the given proof from the end to the starting point is sufficient.
 \end{proof}
 
+\begin{lemma}
+	Then the following propositions hold:
+	\begin{enumerate}
+		\item $\powf\pi_2\comp\supseteq\comp(\powf\pi_1)^\op\quad=\quad\supseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$
+		\item $\powf\pi_1\comp\supseteq\comp(\powf\pi_2)^\op\quad=\quad\supseteq\comp \powf\pi_1\comp(\powf\pi_2)^\op$
+	\end{enumerate}
+\end{lemma}
+\begin{proof}
+	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op\quad=\quad\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$.
+	
+	Assuming $x \mathrel{\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that
+	\begin{gather*}
+		z \mathrel{(\powf\pi_i)} x,\\
+		z \mathrel{\subseteq} z',\\
+		z'\mathrel{(\powf\pi_j)} y.
+	\end{gather*}
+	Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\supseteq\comp \powf\pi_j} y$, thus $x\mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$.
+	
+	Now, assuming $x \mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
+	\begin{gather*}
+		z\mathrel{(\powf\pi_i)} x,\\
+		z \mathrel{(\powf\pi_j)} y',\\
+		y' \mathrel{\subseteq} y.
+	\end{gather*}
+	We take the set $w=z\cup \powf\pi_i(z)\times y$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$,  $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op} y$.\qed
+\end{proof}
+	
+%\begin{lemma}
+%	Assuming that $F\pi_1$ and $F\pi_2$ are monotone with respect to $\sqsubseteq$ that is an order over $F$, then the following propositions hold:
+%	\begin{enumerate}
+%		\item $F\pi_2\comp\sqsupseteq\comp(F\pi_1)^\op\quad=\quad\sqsupseteq\comp F\pi_2\comp(F\pi_1)^\op$
+%		\item $F\pi_1\comp\sqsupseteq\comp(F\pi_2)^\op\quad=\quad\sqsupseteq\comp F\pi_1\comp(F\pi_2)^\op$
+%	\end{enumerate}
+%\end{lemma}
+%\begin{proof}
+%	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op\quad=\quad\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op$.
+%	
+%	Assuming $x \mathrel{F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
+%	\begin{gather*}
+%		z \mathrel{(F\pi_i)} x,\\
+%		z \mathrel{\sqsubseteq} z',\\
+%		z'\mathrel{(F\pi_j)} y.
+%	\end{gather*}
+%	Then from $z \mathrel{\sqsubseteq} z'$ we get $F\pi_j(z)\mathrel{\sqsubseteq}y$. So, we have $z\mathrel{\sqsupseteq\comp F\pi_j} y$, thus $x\mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$.
+%	
+%	Now, assuming $x \mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
+%	\begin{gather*}
+%		z\mathrel{(F\pi_i)} x,\\
+%		z \mathrel{(F\pi_j)} y',\\
+%		y' \mathrel{\sqsubseteq} y.
+%	\end{gather*}
+%\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}
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
-\begin{prop}
-	The following propositions hold:
-	\begin{itemize}
-		\item $\powf\pi_2\comp\supseteq\comp(\powf\pi_1)^\op\quad=\quad\supseteq\comp\powf\pi_2\comp(\powf\pi_1)^\op$
-		\item $\powf\pi_1\comp\supseteq\comp(\powf\pi_2)^\op\quad=\quad\supseteq\comp\powf\pi_1\comp(\powf\pi_2)^\op$
-	\end{itemize}
-\end{prop}
+
 \end{document}