diff --git a/draft/draft.tex b/draft/draft.tex index f2721b5..0f07a57 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2239,7 +2239,9 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \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*}\qed + \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. \end{proof} \begin{prop}