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

minor

Browse Source
This commit is contained in:
partowp 2026-05-20 12:38:25 +01:00
parent f2f207936e
commit c4b7a43bce
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
draft/draft.tex
View File

@ -2244,7 +2244,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\end{proof}
\begin{lemma}
Then the following propositions hold:
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$
@ -2267,7 +2267,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
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\supseteq\comp(\powf\pi_i)^\op} y$.\qed
\end{proof}
%\begin{lemma}