From 3d9820468495d99d77748e7c33efcdf0f68c5f46 Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 21 May 2026 13:55:20 +0100 Subject: [PATCH 1/6] 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} From a0ace67136685fd9b8f09e555cbe896810b1555b Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 15:29:09 +0100 Subject: [PATCH 2/6] abstract proof --- draft/draft.tex | 76 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 54 insertions(+), 22 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 36a5a23..60e8a99 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1025,12 +1025,12 @@ We show this relation with $F_\rel(R,X)$. X \& R \& X \\ FX \& (FR)^\dagger \& FX \arrow["\alpha"', from=1-1, to=2-1] - \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] + \arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2] \arrow["{p_1}"', from=1-2, to=1-1] \arrow["{p_2}", from=1-2, to=1-3] \arrow["\sigma", from=1-2, to=2-2] \arrow["\alpha", from=1-3, to=2-3] - \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3] \arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1] \arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3] \end{tikzcd} @@ -1123,7 +1123,7 @@ We show this relation with $F_\rel(R,X)$. \end{proof} % Now, we give a counter example of a symmetric relation on $\Set$ that is a simulation according to~\autoref{def:sim}, i.e, exists the morphism $\sigma$ that commutes laxly in~\eqref{eq:diag-lax-sim}, but $\sigma$ is not a coalgebraic bisimulation, although the relation that we give is clearly a bisimulation in the classic sense. -We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\sqsubseteq=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions: +We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\appr=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions: \begin{gather*} A\to C_1\qquad B\to C_2\qquad C_1\to C_1\qquad C_2\to C_2\qquad C'_2\to C_2 \end{gather*} @@ -2214,7 +2214,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i =&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{align*}\qed \end{proof} \begin{prop} $\hat{L}$ is a Barr relator. @@ -2224,10 +2224,10 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{proof} \begin{definition}[One-sided Barr relator] - Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\sqsubseteq$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{one-sided Barr relator} iff we have: + Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{one-sided Barr relator} iff we have: % A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, 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*} - \overrightarrow{F}r=F\pi_2\comp\sappr\comp(F\pi_1)^\op + \overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op \end{gather*} \end{definition} @@ -2239,17 +2239,17 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \begin{align*} s \;\hat{\overrightarrow{F}}r\; t&\\ &\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\ - &\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\sappr\comp(F\pi_2)^\op)^\op\;t\\ - &\iff s\;F\pi_2\comp\sappr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t + &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\ + &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \end{align*} Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and: \begin{gather*} - w\;F\pi_2\comp\sappr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t + w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t \end{gather*} And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and: \begin{align*} - &w\;\sappr\; v \qquad\&\qquad w\;\appr\; v\\ - \iff&(F\pi_1)^\op(s)\;\sappr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\ + &w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\ + \iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\ \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 @@ -2258,31 +2258,31 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i 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{lemma} - The following propositions hold: +\begin{prop} + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ the following propositions hold: \begin{enumerate} - \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$ + \item $\powf\pi_2\comp\subseteq\comp(\powf\pi_1)^\op\quad=\quad\subseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$ + \item $\powf\pi_1\comp\subseteq\comp(\powf\pi_2)^\op\quad=\quad\subseteq\comp \powf\pi_1\comp(\powf\pi_2)^\op$ \end{enumerate} -\end{lemma} +\end{prop} \begin{proof} - Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op\quad=\quad\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$. + Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op\quad=\quad\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$. - Assuming $x \mathrel{\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that + Assuming $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that \begin{gather*} z \mathrel{(\powf\pi_i)} x,\\ z \mathrel{\subseteq} z',\\ z'\mathrel{(\powf\pi_j)} y. \end{gather*} - Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\supseteq\comp \powf\pi_j} y$, thus $x\mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$. + Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\subseteq\comp \powf\pi_j} y$, thus $x\mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$. - Now, assuming $x \mathrel{\supseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that + Now, assuming $x \mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that \begin{gather*} z\mathrel{(\powf\pi_i)} x,\\ z \mathrel{(\powf\pi_j)} y',\\ y' \mathrel{\subseteq} y. \end{gather*} - We take the set $w=z\cup (\powf\pi_i(z)\times y)$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$, $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\supseteq\comp(\powf\pi_i)^\op} y$.\qed + We take the set $w=z\cup (\powf\pi_i(z)\times y)$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$, $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$.\qed \end{proof} %\begin{lemma} @@ -2310,7 +2310,39 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i % y' \mathrel{\sqsubseteq} y. % \end{gather*} %\end{proof} - +\begin{definition}[Cogood Order Structure]\label{def:cogood} + A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that: + \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] + \item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$ and $g\c Y\to Y'$, then $Fg\comp\alpha\comp f\appr Fg\comp\beta\comp f$ in $\Hom(X',Y')$.\label{item:cogood:I} + \item If $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\label{item:cogood:II} + \end{enumerate} +\end{definition} +\begin{prop} + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is has a cogood order structure $\appr$, the following propositions hold: + \begin{enumerate} + \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$ + \item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ + \end{enumerate} +\end{prop} +\begin{proof} + Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$. + + Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that + \begin{gather*} + z \mathrel{(F\pi_i)} x,\\ + z \mathrel{\appr} z',\\ + z'\mathrel{(F\pi_j)} y. + \end{gather*} + Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$. + + Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that + \begin{gather*} + z\mathrel{(F\pi_i)} x,\\ + z \mathrel{(F\pi_j)} y',\\ + y' \mathrel{\appr} y. + \end{gather*} + Since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:II} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed +\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 relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator. \end{prop} From 46e6f44bd4a154f759ef8b7f32094631b94d1b79 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 15:57:32 +0100 Subject: [PATCH 3/6] minor --- draft/draft.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 60e8a99..aeb3f02 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2318,7 +2318,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{enumerate} \end{definition} \begin{prop} - For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is has a cogood order structure $\appr$, the following propositions hold: + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold: \begin{enumerate} \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$ \item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ @@ -2344,7 +2344,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i Since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:II} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed \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 relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator. + 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} \begin{proof} \todo{Finish.} From 60a18af74995291a19e0555646f20a7305f42c3f Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 17:34:13 +0100 Subject: [PATCH 4/6] minor --- draft/draft.tex | 51 +++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index aeb3f02..1336985 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2223,8 +2223,8 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \todo{Finish.} \end{proof} -\begin{definition}[One-sided Barr relator] - Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{one-sided Barr relator} iff we have: +\begin{definition}[Mid-lax Barr relator] + Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have: % A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, 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*} \overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op @@ -2232,30 +2232,31 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{definition} \begin{prop} - For every functor $F\c\Set\to\Set$, the symmetrization of the one-sided Bar relator is equal with the Barr relator. + For every functor $F\c\Set\to\Set$, the symmetrization of the mid-lax Bar relator is equal with the Barr relator. \end{prop} \begin{proof} - Where there exist $\pi_1\c A\to X$ and $\pi_2\c A\to Y$ such that $r=\pi_2\comp\pi_1^\op$, we assume that $s \;\hat{\overrightarrow{F}}r\; t$, and we need to show that $s\;F\pi_2\comp(F\pi_1)^\op\;t$. Considering that $r^\op=\pi_1\comp\pi_2^\op$, we have: - \begin{align*} - s \;\hat{\overrightarrow{F}}r\; t&\\ - &\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\ - &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\ - &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t - \end{align*} - Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and: - \begin{gather*} - w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t - \end{gather*} - And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and: - \begin{align*} - &w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\ - \iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\ - \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*} - 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. +% Where there exist $\pi_1\c A\to X$ and $\pi_2\c A\to Y$ such that $r=\pi_2\comp\pi_1^\op$, we assume that $s \;\hat{\overrightarrow{F}}r\; t$, and we need to show that $s\;F\pi_2\comp(F\pi_1)^\op\;t$. Considering that $r^\op=\pi_1\comp\pi_2^\op$, we have: +% \begin{align*} +% s \;\hat{\overrightarrow{F}}r\; t&\\ +% &\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\ +% &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\ +% &\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t +% \end{align*} +% Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and: +% \begin{gather*} +% w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t +% \end{gather*} +% And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and: +% \begin{align*} +% &w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\ +% \iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\ +% \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*} +% 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. +\todo{Finish.} \end{proof} \begin{prop} @@ -2313,7 +2314,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \begin{definition}[Cogood Order Structure]\label{def:cogood} A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that: \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] - \item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$ and $g\c Y\to Y'$, then $Fg\comp\alpha\comp f\appr Fg\comp\beta\comp f$ in $\Hom(X',Y')$.\label{item:cogood:I} + \item If $\alpha\appr\beta$ in $\Hom(X,FY)$, $g\c Y\to Y'$, then $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,Y')$.\label{item:cogood:I} \item If $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.\label{item:cogood:II} \end{enumerate} \end{definition} From 85750ee1eed3f0c23abccf99b7609ee68fbc069a Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 17:46:15 +0100 Subject: [PATCH 5/6] some props to prove --- draft/draft.tex | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/draft/draft.tex b/draft/draft.tex index 1336985..443c1d9 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2311,6 +2311,16 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i % y' \mathrel{\sqsubseteq} y. % \end{gather*} %\end{proof} +\begin{prop} + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is either the maybe monad, the subdistribution monad or $FX=\powf(X\times A)$, where $A$ is a set of labels, then the following propositions hold: + \begin{enumerate} + \item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$ + \item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ + \end{enumerate} +\end{prop} +\begin{proof} + \todo{Finish.} +\end{proof} \begin{definition}[Cogood Order Structure]\label{def:cogood} A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that: \begin{enumerate}[label=(\Roman*), ref=(\Roman*)] @@ -2344,6 +2354,39 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \end{gather*} Since $\appr$ is a cogood order structure by~\autoref{def:cogood}.\ref{item:cogood:II} there exists a $w$ such that $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$, $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed \end{proof} +\begin{prop} + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold: + \begin{enumerate} + \item $F\pi_2\comp\sappr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$ + \item $F\pi_1\comp\sappr\comp(F\pi_2)^\op\quad=\quad F\pi_1\comp(F\pi_2)^\op\comp\appr$ + \end{enumerate} +\end{prop} +\begin{proof} + \todo{Finish.} +\end{proof} +\begin{prop} + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold: + \begin{enumerate} + \item $F\pi_2\comp\appr\comp\sappr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op\comp\appr$ + \item $F\pi_1\comp\appr\comp\sappr\comp(F\pi_2)^\op\quad=\quad \appr\comp F\pi_1\comp(F\pi_2)^\op\comp\appr$ + \end{enumerate} +\end{prop} +\begin{proof} + \todo{Finish.} +\end{proof} +\begin{prop} + For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a good order structure $\appr$, the following propositions hold: + \begin{enumerate} + \item $F\pi_2\comp\sappr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$ + \item $F\pi_1\comp\sappr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$ + \end{enumerate} +\end{prop} +\begin{proof} + \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. +\end{prop} \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} From ac7303d14a4fffb11746c62301fa7a0a0acc9465 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 22 May 2026 17:51:31 +0100 Subject: [PATCH 6/6] 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}