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

pc sync

Browse Source
This commit is contained in:
Sergey Goncharov
2026-06-09 20:53:59 +01:00
parent aea41d1451
commit d07e21f341
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+1 -1
View File
@@ -2343,7 +2343,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\end{enumerate} \end{enumerate}
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
$(I)$ Assuming $t\mathrel{Ff\comp\sappr} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is good, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{\sappr\comp Ff} x$. $(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is good, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{\sappr\comp Ff} x$.
Assuming $t\mathrel{\sappr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:good-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$. Assuming $t\mathrel{\sappr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:good-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$.