diff --git a/draft/draft.tex b/draft/draft.tex index ab9b52b..f67805b 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2321,13 +2321,33 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \begin{proof} \todo{Finish.} \end{proof} -\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{definition}[Natural Order Structure]\label{def:nat-ord} + A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X\to X'$, $g\c Y\to Y'$, then: \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] - \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} + \item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',Y)$. \label{item:nat-ord:I} + \item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$. \label{item:nat-ord:II} \end{enumerate} \end{definition} +\begin{definition}[Good Order Structure]\label{def:good-ord} + A \emph{good order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr Fg\comp k$ 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'$. +\end{definition} +\begin{definition}[Cogood Order Structure]\label{def:cogood-ord} + A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and 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'$. +\end{definition} +\begin{lemma} + Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, then for every $f\in\Hom(X,FY)$ we have: + \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] + \item $Ff\comp\appr\quad=\quad\appr\comp Ff$ + \item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$ + \end{enumerate} +\end{lemma} +\begin{proof} + $(I)$Assuming $t\mathrel{Ff\comp\appr} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is good, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{\appr\comp Ff} x$. + + Assuming $t\mathrel{\appr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:cogood-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$. + + $(II)$\todo{Finish.} +\end{proof} \begin{prop} For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold: \begin{enumerate} @@ -2344,7 +2364,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i z \mathrel{\appr} z',\\ z'\mathrel{(F\pi_j)} y. \end{gather*} - Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$. + Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$. Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that \begin{gather*} @@ -2352,7 +2372,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i z \mathrel{(F\pi_j)} y',\\ y' \mathrel{\appr} y. \end{gather*} - Since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:II} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed + Since $\appr$ is a cogood order structure by~\autoref{def:cogood-ord} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed \end{proof} \begin{prop} For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold: