diff --git a/draft/draft.tex b/draft/draft.tex index 443c1d9..ab9b52b 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2385,8 +2385,11 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \todo{Finish.} \end{proof} \begin{prop} - Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that take $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator. + Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator. \end{prop} +\begin{proof} + \todo{Finish.} +\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 symmetrization of the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator. \end{prop}