bluh

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_F=F\\
-		SP_Ff=Ff,\;TP_Ff=Ff\\
+		TP_F=F\\
-		P_FX=P_FX\odot P_FX\\
+		P_F=\odot\comp\Delta\comp P_F
-		P_Ff=P_Ff\odot P_Ff
 	\end{gather*}
 \end{definition}
 %