From dc05b47c2b0532313675572c79349d262536d7eb Mon Sep 17 00:00:00 2001
From: partowp <partowp@UOB25BXTXG74.adf.bham.ac.uk>
Date: Tue, 19 May 2026 18:19:59 +0100
Subject: [PATCH] prop

---
 draft/draft.tex | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/draft/draft.tex b/draft/draft.tex
index 159161d..3e200c5 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -2248,6 +2248,13 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
+\begin{prop}
+	The following propositions hold:
+	\begin{itemize}
+		\item $\powf\pi_2\comp\supseteq\comp(\powf\pi_1)^\op\quad=\quad\supseteq\comp\powf\pi_2\comp(\powf\pi_1)^\op$
+		\item $\powf\pi_1\comp\supseteq\comp(\powf\pi_2)^\op\quad=\quad\supseteq\comp\powf\pi_1\comp(\powf\pi_2)^\op$
+	\end{itemize}
+\end{prop}
 \end{document}