diff --git a/draft/draft.tex b/draft/draft.tex index 63c887b..f2721b5 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2228,11 +2228,11 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i &\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\sappr\comp(F\pi_2)^\op)^\op\;t\\ &\iff s\;F\pi_2\comp\sappr\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 function, then $(F\pi_1)^\op$ is an injective map, so there exist exactly 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*} w\;F\pi_2\comp\sappr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t \end{gather*} - And similarly, since $F\pi_2$ is also a function we have exactly 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*} &w\;\sappr\; v \qquad\&\qquad w\;\appr\; v\\ \iff&(F\pi_1)^\op(s)\;\sappr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\