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-22 17:51:31 +01:00
parent 85750ee1ee
commit ac7303d14a
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
draft/draft.tex
View File

@ -2385,8 +2385,11 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\todo{Finish.} \todo{Finish.}
\end{proof} \end{proof}
\begin{prop} \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} \end{prop}
\begin{proof}
\todo{Finish.}
\end{proof}
\begin{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. 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} \end{prop}