diff --git a/draft/draft.tex b/draft/draft.tex index 3226228..dabc7cb 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2087,13 +2087,13 @@ Given an $F$-relator $\relar$ defined in~\autoref{def:relator} we have a canonic For a category $\BC_0$ with pullbacks and an endofunctor $F$ on it, every abstract relational bisimulation (\autoref{def:abs-rel-bis}) is an $\rel(F)$-double coalgebra that $\rel(F)$ is the map that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to a relation $(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$. It entails that every Hermida-Jacobs bisimulation is also an $(F-)^\dagger$-double coalgebra if we conceive $(F-)^\dagger$ as the proper double relator. \end{example} % +Using the basic fact in $\Set$ that a relation $R\subseteq X\times X$ is a poset iff $R\comp R=R$, we define poset enrichment abstractly as follows: \begin{definition}[Poset-enrichment Functor] - On a double category $\BC_1\rightrightarrows\BC_0$, for a functor $F\c\BC_0\to\BC_0$ a functor $P_F\c\BC_0\to\BC_1$ is a \emph{poset-enrichment} functor over $F$ such that for every objects $X$ and mrphisms $f$, the following equations hold: + On a double category $\BC_1\rightrightarrows\BC_0$, for a functor $F\c\BC_0\to\BC_0$ a functor $P_F\c\BC_0\to\BC_1$ is a \emph{poset-enrichment} functor over $F$ such that for every objects $X$ and mrphisms $f$, the following equations hold ($\Delta$ is the diagonal functor): \begin{gather*} - SP_FX=FX,\;TP_FX=FX\\ - SP_Ff=Ff,\;TP_Ff=Ff\\ - P_FX=P_FX\odot P_FX\\ - P_Ff=P_Ff\odot P_Ff + SP_F=F\\ + TP_F=F\\ + P_F=\odot\comp\Delta\comp P_F \end{gather*} \end{definition} %