minor

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}