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

Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

Browse Source
This commit is contained in:
partowp
2026-07-20 19:01:48 +01:00
parent 61fed4f74a 9da15b278c
commit 944bd831b6
1 changed files with 2 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+2 -3
View File
@@ -2163,8 +2163,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
% We have $(Fp_1)^\dagger\comp\sigma$. % We have $(Fp_1)^\dagger\comp\sigma$.
%\end{proof} %\end{proof}
\begin{example} \begin{example}
And another counter-example!!! Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. Let us call this functor $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. We show the functor with $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below: We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
\begin{gather*} \begin{gather*}
\alpha(x)= \alpha(x)=
@@ -3239,7 +3238,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
\end{align*}\qed \end{align*}\qed
\end{proof} \end{proof}
\begin{cor} \begin{cor}
Since the symmetrization of left-lax Barr relator that is laxed with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator. Since the symmetrization of left-lax Barr relator with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
\end{cor} \end{cor}
\begin{cor} \begin{cor}
By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well. By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well.