From e60e3d4a1d53bede9b87a730cafd53e04b8a0c01 Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 5 May 2026 16:50:22 +0100 Subject: [PATCH] does it work? --- draft/draft.tex | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/draft/draft.tex b/draft/draft.tex index dda809e..9124826 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2149,6 +2149,17 @@ 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} +\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. +\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. +\end{proof} \end{document}