From 46e6f44bd4a154f759ef8b7f32094631b94d1b79 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 15:57:32 +0100 Subject: [PATCH] minor --- draft/draft.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 60e8a99..aeb3f02 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2318,7 +2318,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{enumerate} \end{definition} \begin{prop} - For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is has a cogood order structure $\appr$, the following propositions hold: + 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} \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$ \item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ @@ -2344,7 +2344,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i 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 \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. + 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 symmetrization of 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.}