From 3d9820468495d99d77748e7c33efcdf0f68c5f46 Mon Sep 17 00:00:00 2001
From: partowp <partowp@UOB25BXTXG74.adf.bham.ac.uk>
Date: Thu, 21 May 2026 13:55:20 +0100
Subject: [PATCH] a proof

---
 draft/draft.tex | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/draft/draft.tex b/draft/draft.tex
index 9cfac8c..36a5a23 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2194,13 +2194,28 @@ For every relation $r\rto X\to Y$ $\emre r=\subseteq\;\emre r=\emre r\;\subseteq
 
 Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.
 
-\begin{definition}
+\begin{definition}[Barr relator]
 	A relator over a functor $F$ is a Barr relator, shown by $\bar{F}$, iff for a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
 	\begin{gather*}
 		\bar{F}r=F\pi_2\comp(F\pi_1)^\op
 	\end{gather*}
 \end{definition}
-
+\begin{prop}
+	For every set-functor $F$, the barr relator $\bar{F}$ is symmetric.
+\end{prop}
+\begin{proof}
+	Assuming that for a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ we have $r=\pi_2\comp\pi_1^\op$, then we have:
+	\begin{align*}
+		\hat{\bar{F}}r&\\
+		=&\bar{F}r\cap(\bar{F}r^\op)^\op\\
+		=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_2\comp\pi_1^\op)^\op)^\op\\
+		=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_1\comp\pi_2^\op))^\op\\
+		=&F\pi_2\comp(F\pi_1)^\op\cap(F\pi_1\comp (F\pi_2)^\op)^\op\\
+		=&F\pi_2\comp(F\pi_1)^\op\cap F\pi_2\comp (F\pi_1)^\op\\
+		=&F\pi_2\comp(F\pi_1)^\op\\
+		=&\bar{F}r
+	\end{align*}
+\end{proof}
 \begin{prop}
 	$\hat{L}$ is a Barr relator.
 \end{prop}