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

some props to prove

Browse Source
This commit is contained in:
partowp 2026-05-22 17:46:15 +01:00
parent 60a18af749
commit 85750ee1ee
1 changed files with 43 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
draft/draft.tex
View File

@ -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}