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

definitions

Browse Source
This commit is contained in:
partowp 2026-04-28 14:23:01 +01:00
parent 484bb73af8
commit 53255e898c
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
draft/draft.tex
View File

@ -1940,7 +1940,7 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
\end{definition}
\begin{definition}[Hermida-Jacobs Simulation]
For a relator $\relar$ on a functor $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
For a relator $\relar$ on a functor $F$ a HJ-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
\begin{equation*}\label{def:hej-sim}
\begin{tikzcd}[ampersand replacement=\&]
X \& r \& Y \\
@ -1955,6 +1955,10 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
\end{tikzcd}
\end{equation*}
\end{definition}
\begin{definition}[Relator-based Simulation]
Given a relator $\relar$, a relation $r\c X\rto Y$ is an $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \beta^\op\comp\relar R\comp \alpha$, i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$.
\end{definition}
\begin{prop}
For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique.
\end{prop}