From ac7303d14a4fffb11746c62301fa7a0a0acc9465 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 17:51:31 +0100 Subject: [PATCH] minor --- draft/draft.tex | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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}