From 107d2d0efb0daf0f1ab2eb151fabd5c3fb8c828a Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 5 May 2026 18:26:02 +0100 Subject: [PATCH] more props added --- draft/draft.tex | 36 +++++++++++++++++++++++++++++------- 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 9124826..1c9decb 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -288,6 +288,7 @@ \newcommand{\gra}{\mathbf{Gra}} \newcommand{\obj}{\mathbf{Obj}} \newcommand{\relar}{\mathbf{R}} +\newcommand{\emre}{\mathbf{L}} \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}} \newcommand{\powf}{\mathcal{P}} @@ -2149,16 +2150,37 @@ then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in \begin{cor} Assuming that a relator $\relar$ over a functor $F\c\Set\to\Set$ satisfies $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$ for every functions $f\c X\to Z$ and $g\c Y\to Z$, then $\hat{\relar}$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete, using the axiom of choice. \end{cor} +\subsection{Egli-Milner relator} +\begin{definition} + We call the map $\emre\c\rel\to\rel$ the Egli-Milner $\powf$-relator, whenever for every relation $r\c X\rto Y$ it is defined as follows: + \begin{gather*} + \emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\} + \end{gather*} +\end{definition} +Egli-Milner relator is not sound or complete, although its symmetrization is sound and complete. \begin{prop} - Assuming that for a relator $\relar$ over $F\c\Set\to\Set$, $\hat{\relar}$ is difunctionally functorial, then $\relar$ is also difunctionally functorial, and vice-versa. + $\hat{\emre}$-similarity from a coalgebra $(\alpha,X)$ to $(\beta,Y)$ is sound and complete. \end{prop} \begin{proof} - $\hat{\relar}$ being difunctionally functorial means that for every functions $f\c X\to FX$ and $g\c Y\to FY$, we have $\hat{\relar}(g^\op\comp f)=(Fg)^\op\comp Ff$. It is equivalent with the both following conditions being true: - \begin{itemize} - \item ${\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$, or $({\relar}(f^\op\comp g))^\op\leq(Fg)^\op\comp Ff$ - \item ${\relar}(g^\op\comp f)\geq(Fg)^\op\comp Ff$ and $({\relar}(f^\op\comp g))^\op\geq(Fg)^\op\comp Ff$ - \end{itemize} - The proof from right to left is obvious. For the other direction we assume that $\hat{\relar}$ is difunctinally functorial. Then we have $\hat{\relar}(g^\op\comp f)\leq(Fg)^\op\comp Ff$ and $\hat{\relar}(g^\op\comp f)\geq(Fg)^\op\comp Ff$. The earlier gives the first item, and the later gives the second item. + \todo{Finish.} +\end{proof} +The symmetrization of the Egli-Milner relator is a Barr-relator. Barr-relators is a generalization of the Egli-Milner relator, where the functor is generalized. + +\begin{prop} + Assuming that $r\c X\rto Y$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then $\appr_{X};\hat{\emre};\appr_{Y}=\appr_{X};\hat{\emre}$ and $\appr_{X};\hat{\emre}=\hat{\emre};\appr_{Y}$. +\end{prop} + +\begin{definition} + A relator over a functor $F$ is a Barr-relator, shown by $\bar{F}$, iff for 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*} + \bar{F}r=F\pi_2\comp(F\pi_1)^\op + \end{gather*} +\end{definition} +\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}