pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

removed non-src files

Browse Source
This commit is contained in:
Sergey Goncharov 2026-05-20 18:04:38 +01:00
commit b72e235839
7 changed files with 149 additions and 147 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
ACV-abstract-2026/big-step-short.cit
View File

@ -1 +0,0 @@
d41d8cd98f00b204e9800998ecf8427e -

10
ACV-abstract-2026/references.bib
View File

@ -6232,3 +6232,13 @@
doi = {10.4230/LIPIcs.ITP.2019.30},
timestamp = {Sat, 05 Sep 2020 18:04:33 +0200}
}
@article{Dubut25,
title={Aczel-mendler bisimulations in a regular category},
author={Dubut, J{\'e}r{\'e}my},
journal={Logical Methods in Computer Science},
volume={21},
year={2025},
publisher={Episciences. org}
}

119
ACV-abstract-2026/review.txt
View File

@ -1,119 +0,0 @@
CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.
Dear Sergey,
On behalf of the Programme Committee of CALCO 2025, we are happy to inform you that your early idea contribution 11
From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
has been accepted for presentation at CALCO 2025.
The reviews for your submission are attached below. Please take the reviewer comments into account when preparing the final version. More details regarding the final version will follow shortly.
We look forward to seeing you in Glasgow!
Best regards,
Corina and Alexander.
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
----------------------- REVIEW 1 ---------------------
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas
----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
This "early idea" abstract on abstract big-step semantics through abstract higher-order GSOS (AHOGSOS) is well in scope of CALCO.
I see no reason to reject it.
That said, I am not an expert on GSOS and I failed to understand the technical content of this abstract. I made an honest attempt, and my comments below could be seen as a proof-of-work.
The failure to communicate might be due to the lack of space the authors had for the presentation, but I also see some essential shortcoming. Half a page, that is 25% of the total available space of 2 pages, is spent on the example of combinatory logic (CL), but then the example is not connected to the abstract framework it was intended to illustrate.
Very concretely, the functors Σ and B should be instantiated to CL, and then also the refinement of them presented in the "separability" part.
The question is whether then there is enough space remaining for all of the content of the abstract. If I had to make the choice, I would put the counterexample (l55ff) into a technical report and link to it from the abstract. This counterexample takes around 15% of the total space, and these 15% could be used instead to connect the abstract framework to the CL example.
Details
=======
Small-step and big-step semantic for CL are well-presented, but then AHOGSOS is introduced, CL is not connected to its formalism. The question is, why do you prepare the reader by a concrete example just to drop it once you go to the abstract mathematics?
From the level of difficulty, I think when you sit down an implement big-step operational semantics for CL, you quickly converge to the presentation you call xCL where you form "closures" for underapplied uses of K and S. In contrast, an abstract framework for SOS is not something that suggests itself.
Concretely, I am missing answers for the following questions:
1. Category C, what do its objects and morphisms denote?
2. What is the signature functor Σ for the case of xCL?
3. What is the behavior functor B?
4. Likewise what are then Σᵥ, Σ_c, D and T?
My guesses:
1. The objects of C are representing sets of terms, morphisms functions.
2. Σ is the "non-recursive" presentation of the language of xCL, e.g.
```haskell
data Σ X = I | K | S | K' X | S' X | S'' X X | App X X
```
3. Here I am lost with my current background knowledge, as I would expect now some relation specifying the operational semantics, but B targets C.
Reading Turi and Plotkin [4], I might get some more clues.
There, B is the "successor" functor for the operational semantics, producing for a set X of terms the collection B X of terms reachable by a single operational step. This collection B is organized by the labels a ∈ A on the rules of the operational semantics.
The "abstract GSOS" simply speaks of ρX : Σ(X × BX) → B(TX) which comes close to the presentation here assuming that the set TX of terms over X is Σ^⋆X.
Somehow fact that the labels in xCL are also terms materializes in a B : Cᵒᵖ × C → C, but it is not clear to me which of the positions of B are for the labels and which for the lhss.
Guessing that X is for the lhss in accordance with paper [4], I do not understand why B(X,Y) becomes contravariant in X when in [4] it was covariant.
So, if the xCL example shall be of any use in this abstract, B needs to spelled out for xCL.
----------------------- REVIEW 2 ---------------------
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas
----------- Overall evaluation -----------
SCORE: 1 (weak accept)
----- TEXT:
A categorical approach to relate big-step and small-step operational semantics in terms of higher-order GSOS is outlined.
Though well-motivated in principle in a presentation it would seem advantageous to first see the workings of moving between the two operational semantics types on the rule level before diving into the categorical details. In particular, it seems that some of the issues that still have to be solved - the strong separation condition - are best explained with conditions on rules.
----------------------- REVIEW 3 ---------------------
SUBMISSION: 11
TITLE: From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly (Early ideas)
AUTHORS: Sergey Goncharov, Pouya Partow and Stelios Tsampas
----------- Overall evaluation -----------
SCORE: 2 (accept)
----- TEXT:
The paper outlines an approach for relating small-step and big-step
operational semantics in an abstract categorical setting. The authors
build on the existing theory of abstract higher-order GSOS where the
small-step semantics can be specified categorically. This is extended
to a separated higher-order GSOS, separating the the syntax into value
constructors and computation constructors. In this setting one can
define a multistep semantics as least fixpoint and abstract the
big-step semantics as a natural transformation from computation
constructors applied to values to a monad of results.
The authors observe that separability alone is not enough to prove the
fundamental equivalence between small-step and big-step semantics and
identify a stronger condition, which abstracts the idea of suitably
constraining the shape of rule conclusions based on the premises, as a
potential way to remedy this issue.
The theme is surely of interest for CALCO. The authors did a good job
in sythesizing in a limit space the main ideas of their work. For a
non-expert (like me) the technical details are difficult to grasp from
the short summary, but I do not see this as a problem. Rather, I think
this can be a quite interesting and valuable addition to CALCO's program.

BIN
ACV-abstract-2026/sym-sim.pdf
View File

Binary file not shown.

109
ACV-abstract-2026/sym-sim.tex
View File

@ -13,7 +13,18 @@
\usepackage{mdframed, ebproof}
\usepackage{microtype}
\usepackage{stackengine}
\usepackage{tikz-cd}
\usetikzlibrary{arrows.meta}
\usetikzlibrary{decorations} % Required for all decorations
\usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag'
\tikzset{
commutative diagrams/.cd,
arrow style = tikz,
diagrams = {>=stealth},
row sep = large,
column sep = huge
}
\input{catprog}
\renewcommand{\by}[1]{\text{/$\mspace{-2mu}$/~#1}}
@ -59,6 +70,7 @@
\renewcommand{\comp}{\cdot}
\newcommand{\klstar}{\sharp} %% Kleisli star
\newcommand{\relar}{\mathbf{R}}
\title{Soundness and Completeness of Symmetric Relators} %TODO Please add
%Or: It is expected from a symmetric simulation to be a bisimulation
@ -136,37 +148,82 @@
%\section{Mathematical Preliminaries}%\label{sec:}
\paragraph{Compositionality}
Given a labeled transition systems $(S,L,\to)$, where $S$ is a set of states, $L$ is a set of labels, and $\to\subseteq S\times L\times S$ is a set of labeled transitions, a \emph{simulation} is a relation $r\subseteq S\times S$ such that the following sentence holds:
%\paragraph{Compositionality}
%Given a labeled transition systems $(S,L,\to)$, where $S$ is a set of states, $L$ is a set of labels, and $\to\subseteq S\times L\times S$ is a set of labeled transitions, a \emph{simulation} is a relation $r\subseteq S\times S$ such that the following sentence holds:
%\begin{gather*}
% (x,y)\in r, x\xto{l} x' \Rightarrow \exists y', y\xto{l} y' \;\text{ and } (x',y')\in r
%\end{gather*}
%The greatest simulation relation over $S$ is called \emph{similarity} and shown with $\leq$. A simulation relation $r$ on $S$ is a \emph{bisimulation} iff the following sentence holds:
%\begin{gather*}
% (x,y)\in r, y\xto{l} y' \Rightarrow \exists x', x\xto{l} x' \;\text{ and } (x',y')\in r
%\end{gather*}
%The greatest bisimulation relation over $S$ is called \emph{bisimilarity} and shown with $\sim$. This is the traditional definition of bisimilarity. There are many different notions. For this definition, we can say that the symmetric similarity is the bisimilarity. But it is not always true for different notions.
%
%\paragraph{Coalgebraic Bisimulation}
%For an endofunctor $F$ over a category $\BC$, a coalgebra, is a pair $(X,\alpha)$, where $X$ is an object of $\BC$ and $\alpha\c X\to FX$ is a morphism in $\BC$. Coalgebras serve as an abstraction of variant transition systems. For example, a labeled transition system $(S,L,\to)$ is a coalgebra $(S,\gamma)$, where $\gamma\c S\to\mathcal{P}(L\times S)$ and $\mathcal{P}$ is the powerset functor.
%
%$S$ can be the set of the terms of a programming language given by a signature $\Sigma$, and $\to$ can be the set of labeled inductions of the language, given by an operational semantics. Following that, a context $C$ is defined as:
%\begin{gather*}
% C\Coloneqq\Box\mid f(C,\bar{t})\mid f(\bar{t},C)\mid f(\bar{u},C,\bar{s})
%\end{gather*}
%$f\in\Sigma$ and by $\bar{t}$, $\bar{s}$ and $\bar{u}$ we mean vectors of terms in $S$. $\Box$ is a placeholder. Assuming $t\in S$, then $C[t]\in S$. We call a relation $r$ congruence iff for terms $t$ and $s$, and a context $C$, $t\mathrel{r}s$ gives $C[t]\mathrel{r}C[s]$. A language with its operational semantics is compositional iff the bisimilarity relation over the terms of the language is a congruence.
%
%\paragraph{Howe's method}
%Howe's method has been traditionally used for compositionality results. \emph{Howe closure} of a relation $r$ is shown by $\hat{r}$ and is defined with the following inference rule:
%\begin{gather*}
% \infer{f(\bar{t})\mathrel{\hat{r}} s}{\bar{t}\mathrel{\hat{r}} \bar{s} & f(\bar{s})\mathrel{r} s}
%\end{gather*}
%Assuming that $r$ is reflexive, then $r\subseteq\hat{r}$, and $\hat{r}$ is a congruence. Additionally, if $r$ is reflexive and symmetric, then $\hat{r}^\star$, the transitive closure of $\hat{r}$ is symmetric (the transitive closure trick). So, to prove that bisimilarity is a congruence it is sufficient to prove that $\hat{\sim}$ is a bisimulation. Given the non-symmetric nature of the closure, it is more common to prove that $\hat{\sim}$ is a simulation. It is usually expected from a symmetric simulation to be a bisimulation. But it has not always been the case.
%
%\paragraph{Relators}
%There exist various notions of (bi)simulation in the literature. For some of them, it is expected from a symmetric simulation to be a bisimulation. It is true for the most traditionally known notion. A more advanced example is in Howe's method. Howe's method is used to prove that applicative bisimilarity is a congruence. It is done by applying Howe closure on bisimilarity, and then proving that the given relation is a bisimulation. Howe closure of bisimilarity includes it and preserves its symmetry. More importantly, Howe closure of bisimilarity is a congruence. Given the non-symmetric nature of Howe closure, it is more common to prove that applying Howe closure on the bisimilarity, gives a simulation, and then we have the rest. But getting to bisimulation from having a symmetric simulation is a step that we believe needs to be taken with care, and we discuss here.
There exist various notions of (bi)simulation in the literature. It is usually expected from a symmetric simulation to be a bisimulation. It is true for the most traditionally known notion, but such conclusion must be made with care. We describe a scenario, in which we have a proof that a symmetric relation is a simulation, but the proof does not serve as a proof for the relation to be a bisimulation.
We take the Aczel-Mendler simulation\cite{Dubut25}. Given a partial order over a functor $F\c\BC\to\BC$, a relation $r$ on $X$ is a simulation on a coalgebra $(X,\alpha)$ iff there exists a coalgebra $(R,\sigma)$ called \emph{witness} that laxly commutes in the following diagram:
\begin{equation}\label{eq:diag-lax-sim}
\begin{tikzcd}[ampersand replacement=\&]
X \& r \& X \\
FX \& Fr \& FX
\arrow["\alpha"', from=1-1, to=2-1]
\arrow["\sqsubseteq"{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["{{Fp_1}}", from=2-2, to=2-1]
\arrow["{{Fp_2}}"', from=2-2, to=2-3]
\end{tikzcd}
\end{equation}
If~\eqref{eq:diag-lax-sim} commutes fully, then $\sigma$ is a witness for $r$ to be an \emph{Aczel-Mendler bisimulation}.
Assuming that $F=\mathcal{P}$ is the powerset functor on $\Set$, we take $r=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$, and $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below:
\begin{gather*}
(x,y)\in r, x\xto{l} x' \Rightarrow \exists y', y\xto{l} y' \;\text{ and } (x',y')\in r
\sigma(w)=
\begin{cases}
r & w\neq (1,3) \\
r\setminus\{(1,2)\} & w=(1,3)
\end{cases}
\end{gather*}
The greatest simulation relation over $S$ is called \emph{similarity} and shown with $\leq$. A simulation relation $r$ on $S$ is a \emph{bisimulation} iff the following sentence holds:
In this scenario, $\sigma$ is a witness for $r$ to be a simulation, but it is not a witness for $r$ to be a bisimulation, since for every $w\in r$ we have $\alpha(p_1(w))\subseteq\mathcal{P}p_1(\sigma(w))=X$. Also, for every $w\in r$, $\mathcal{P}p_2(\sigma(w))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq\mathcal{P}p_2(\sigma(1,3))=X\setminus\{2\}$.
Inspired by Hermida-Jacobs bisimulation\cite{HermidaJacobs98} we modify the definition by setting $\BC$ to be a regular category, and changing the span $(FR,Fp_1,Fp_2)$ in~\eqref{eq:diag-lax-sim} with the span $((Fr)^\dagger,(Fp_1)^\dagger,(Fp_2)^\dagger)$, where $(Fr)^\dagger$ is the image of $\brks{Fp_1,Fp_2}$, and $\brks{(Fp_1)^\dagger,(Fp_2)^\dagger}\c(FR)^\dagger\to FX\times FX$ is monic, so $(Fr)^\dagger$ is a relation. By the symmetry of $r$ there exists $s\c r\to r$ that we call \emph{swap}, where $p_1\comp s=p_2$ and $p_2\comp s=p_1$. The necessary and sufficient condition for $\sigma$ to be a witness for $r$ to be a bisimulation is that
\begin{gather}\label{eq:nec-suf-sim}
\sigma\comp s=(Fs)^\dagger\comp\sigma
\end{gather}
, i.e., $s$ is a $F$-coalgebra morphism from $\sigma$ to itself. Nevertheless, still we have the following example of the $\sigma\c r\to(Fr)^\dagger$ that is a witness for $r$ to be a simulation over $(X,\alpha)$, but it is not a witness for $r$ to be a bisimulation. Keeping the setting of the previous example, we modify $\sigma$ as follows:
\begin{gather*}
(x,y)\in r, y\xto{l} y' \Rightarrow \exists x', x\xto{l} x' \;\text{ and } (x',y')\in r
\sigma(w)=
\begin{cases}
(X,X) & w\neq (1,3) \\
(X,X\setminus\{2\}) & w=(1,3)
\end{cases}
\end{gather*}
The greatest bisimulation relation over $S$ is called \emph{bisimilarity} and shown with $\sim$. This is the traditional definition of bisimilarity. There are many different notions. For this definition, we can say that the symmetric similarity is the bisimilarity. But it is not always true for different notions.
\paragraph{Coalgebraic Bisimulation}
For an endofunctor $F$ over a category $\BC$, a coalgebra, is a pair $(X,\alpha)$, where $X$ is an object of $\BC$ and $\alpha\c X\to FX$ is a morphism in $\BC$. Coalgebras serve as an abstraction of variant transition systems. For example, a labeled transition system $(S,L,\to)$ is a coalgebra $(S,\gamma)$, where $\gamma\c S\to\mathcal{P}(L\times S)$ and $\mathcal{P}$ is the powerset functor.
$S$ can be the set of the terms of a programming language given by a signature $\Sigma$, and $\to$ can be the set of labeled inductions of the language, given by an operational semantics. Following that, a context $C$ is defined as:
\begin{gather*}
C\Coloneqq\Box\mid f(C,\bar{t})\mid f(\bar{t},C)\mid f(\bar{u},C,\bar{s})
\end{gather*}
$f\in\Sigma$ and by $\bar{t}$, $\bar{s}$ and $\bar{u}$ we mean vectors of terms in $S$. $\Box$ is a placeholder. Assuming $t\in S$, then $C[t]\in S$. We call a relation $r$ congruence iff for terms $t$ and $s$, and a context $C$, $t\mathrel{r}s$ gives $C[t]\mathrel{r}C[s]$. A language with its operational semantics is compositional iff the bisimilarity relation over the terms of the language is a congruence.
\paragraph{Howe's method}
Howe's method has been traditionally used for compositionality results. \emph{Howe closure} of a relation $r$ is shown by $\hat{r}$ and is defined with the following inference rule:
\begin{gather*}
\infer{f(\bar{t})\mathrel{\hat{r}} s}{\bar{t}\mathrel{\hat{r}} \bar{s} & f(\bar{s})\mathrel{r} s}
\end{gather*}
Assuming that $r$ is reflexive, then $r\subseteq\hat{r}$, and $\hat{r}$ is a congruence. Additionally, if $r$ is reflexive and symmetric, then $\hat{r}^\star$, the transitive closure of $\hat{r}$ is symmetric (the transitive closure trick). So, to prove that bisimilarity is a congruence it is sufficient to prove that $\hat{\sim}$ is a bisimulation. Given the non-symmetric nature of the closure, it is more common to prove that $\hat{\sim}$ is a simulation. It is usually expected from a symmetric simulation to be a bisimulation. But it has not always been the case.
\paragraph{Relators}
$\sigma$ is a witness for $r$ to be a simulation since for every $w\in r$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\dagger(\sigma(w)))=X$. Also, for every $w\in r$, $((\mathcal{P}p_2)^\dagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\dagger(\sigma(1,3))=X\setminus\{2\}$.
It worth mentioning that $\sigma$ does not satisfy~\eqref{eq:nec-suf-sim}. But still we do not know if having such $\sigma$ can give us a witness that satisfies~\eqref{eq:nec-suf-sim} or guarantees the existence of such witness.
There is a solution for this problem, if we change the context. If we take our category to be $\Set$, we can talk about a kind of well-studied maps named \emph{relator}. For a set functor $F$, a relator $\relar$ takes a relation $r\subseteq X\times Y$ to another relation $\relar r\subseteq FX\times FY$. A relator is monotone with respect to inclusion. For example, in our alternative for Aczel-Mendler simulation, for every set functor $F$, the map that takes a relation $r$ to $(Fr)^\dagger$ is a relator. We show the reverse of a relation $r$ with $r^\op$, and composition of $r$ with another relation $t$ with $t\comp r$. A relation $r\subseteq X\times Y$ is called $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ iff $r\subseteq \beta\comp\relar r\comp\alpha^\op$. Additionally, a relator is called symmetric iff $\relar (r^\op)=(\relar r)^\op$, and a $\relar$-simulation for a symmetric $\relar$ is called a $\relar$-bisimulation that resembles~\eqref{eq:nec-suf-sim}. $\relar$-similarity and $\relar$-bisimilarity are the greatest $\relar$-simulation and $\relar$-bisimulation, respectively. We call a relator $\relar$ sound iff $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is included in the behavioural equivalence from $(X,\alpha)$ to $(Y,\beta)$, and we call it complete iff the behavioural equivalence is included in the $\relar$-similarity.
\newpage
\bibliography{references}

2
ACV-abstract-2026/sym-sim.vtc
View File

@ -1 +1 @@
\contitem\title{Soundness and Completeness of Symmetric Relators}\author{Sergey Goncharov and Pouya Partow}\page{:1--:2}
\contitem\title{Soundness and Completeness of Symmetric Relators}\author{Sergey Goncharov and Pouya Partow}\page{:1--:3}

57
draft/draft.tex
View File

@ -2209,7 +2209,8 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\end{proof}
\begin{definition}[One-sided Barr relator]
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:
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:
% 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
\end{gather*}
@ -2242,12 +2243,66 @@ 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{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$
\end{enumerate}
\end{lemma}
\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$.
Assuming $x \mathrel{\powf\pi_j\comp\supseteq\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$.
Now, assuming $x \mathrel{\supseteq\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
\end{proof}
%\begin{lemma}
% Assuming that $F\pi_1$ and $F\pi_2$ are monotone with respect to $\sqsubseteq$ that is an order over $F$, then the following propositions hold:
% \begin{enumerate}
% \item $F\pi_2\comp\sqsupseteq\comp(F\pi_1)^\op\quad=\quad\sqsupseteq\comp F\pi_2\comp(F\pi_1)^\op$
% \item $F\pi_1\comp\sqsupseteq\comp(F\pi_2)^\op\quad=\quad\sqsupseteq\comp F\pi_1\comp(F\pi_2)^\op$
% \end{enumerate}
%\end{lemma}
%\begin{proof}
% Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op\quad=\quad\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op$.
%
% Assuming $x \mathrel{F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
% \begin{gather*}
% z \mathrel{(F\pi_i)} x,\\
% z \mathrel{\sqsubseteq} z',\\
% z'\mathrel{(F\pi_j)} y.
% \end{gather*}
% Then from $z \mathrel{\sqsubseteq} z'$ we get $F\pi_j(z)\mathrel{\sqsubseteq}y$. So, we have $z\mathrel{\sqsupseteq\comp F\pi_j} y$, thus $x\mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$.
%
% Now, assuming $x \mathrel{\sqsupseteq\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{\sqsubseteq} y.
% \end{gather*}
%\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}
\begin{proof}
\todo{Finish.}
\end{proof}
\end{document}