minor

draft/draft.tex

@@ -2223,8 +2223,8 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\todo{Finish.}
 \end{proof}
 
-\begin{definition}[One-sided Barr relator]
+\begin{definition}[Mid-lax Barr relator]
-	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 $\appr$ 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:
+	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 $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if 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\appr\comp(F\pi_1)^\op
@@ -2232,30 +2232,31 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \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.
+	For every functor $F\c\Set\to\Set$, the symmetrization of the mid-lax 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:
+%	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*}
+%	\begin{align*}
-		s \;\hat{\overrightarrow{F}}r\; t&\\
+%		s \;\hat{\overrightarrow{F}}r\; t&\\
-		&\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\
+%		&\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\
-		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\
+%		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\
-		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
+%		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
-	\end{align*}
+%	\end{align*}
-	Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
+%	Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
-	\begin{gather*}
+%	\begin{gather*}
-		w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
+%		w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
-	\end{gather*}
+%	\end{gather*}
-	And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
+%	And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
-	\begin{align*}
+%	\begin{align*}
-		&w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\
+%		&w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\
-		\iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\
+%		\iff&(F\pi_1)^\op(s)\;\appr\; (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&(F\pi_1)^\op(s)\;=\; (F\pi_2^\op)(t)\\
-		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
+%		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
-		\iff&s\;\bar{F}r\;t
+%		\iff&s\;\bar{F}r\;t
-	\end{align*}
+%	\end{align*}
-	So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
+%	So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
-	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.
+%	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.
+\todo{Finish.}
 \end{proof}
 
 \begin{prop}
@@ -2313,7 +2314,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{definition}[Cogood Order Structure]\label{def:cogood}
 	A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
-		\item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$ and $g\c Y\to Y'$, then $Fg\comp\alpha\comp f\appr Fg\comp\beta\comp f$ in $\Hom(X',Y')$.\label{item:cogood:I}
+		\item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $g\c Y\to Y'$, then $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$.\label{item:cogood:I}
 		\item 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'$.\label{item:cogood:II}
 	\end{enumerate}
 \end{definition}