From 60a18af74995291a19e0555646f20a7305f42c3f Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 17:34:13 +0100 Subject: [PATCH] minor --- draft/draft.tex | 51 +++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index aeb3f02..1336985 100644 --- a/draft/draft.tex +++ b/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] - 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: +\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{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: - \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\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 - \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: - \begin{gather*} - w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t - \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: - \begin{align*} - &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)\;=\; (F\pi_2^\op)(t)\\ - \iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\ - \iff&s\;\bar{F}r\;t - \end{align*} - 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. +% 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\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 +% \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: +% \begin{gather*} +% w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t +% \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: +% \begin{align*} +% &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)\;=\; (F\pi_2^\op)(t)\\ +% \iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\ +% \iff&s\;\bar{F}r\;t +% \end{align*} +% 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. +\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}