more!

draft/draft.tex

@@ -1205,7 +1205,7 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta
 		\end{tikzcd}
 	\end{equation*}
 \end{definition}	
-\begin{definition}[Abstract Relational Bisimulation]
+\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis}
 	In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$.   
 \end{definition}
 The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}.
@@ -2043,13 +2043,72 @@ Given an $F$-relator $\relar$ defined in~\autoref{def:relator} we have a canonic
 	For a category $\BC_0$ with pullbacks, every Aczel-Mendler bisimulation is an $\relar$-double coalgebra that $\relar$ is the map that takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to a span $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.
 \end{example}
 %
-\begin{definition}[Barr Double Relator]
-	\todo{Finish}
+\begin{definition}[Horizontal Lifting]
+	In a double category $\BC_1\rightrightarrows\BC_0$, assuming that $F$ is an endofunctor on $\BC_0$, a lifting of $F$ that we denote with $\bar{F}$ is an endofunctor on $\BC_1$ such that the following diagrams commute:
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			{\BC_1} \& {\BC_1} \& {\BC_1} \& {\BC_1} \\
+			{\BC_0} \& {\BC_0} \& {\BC_0} \& {\BC_0} \\
+			\& {\BC_0} \& {\BC_0} \\
+			\& {\BC_1} \& {\BC_1} \\
+			{\BC_2} \&\&\& {\BC_1} \\
+			\&\&\& {\BC_1}
+			\arrow["{\bar{F}}", from=1-1, to=1-2]
+			\arrow["S"', from=1-1, to=2-1]
+			\arrow["S", from=1-2, to=2-2]
+			\arrow["{\bar{F}}", from=1-3, to=1-4]
+			\arrow["T"', from=1-3, to=2-3]
+			\arrow["T", from=1-4, to=2-4]
+			\arrow["F"', from=2-1, to=2-2]
+			\arrow["F"', from=2-3, to=2-4]
+			\arrow["F", from=3-2, to=3-3]
+			\arrow["U"', from=3-2, to=4-2]
+			\arrow["U", from=3-3, to=4-3]
+			\arrow["{\bar{F}}"', from=4-2, to=4-3]
+			\arrow["{-\odot-}", from=5-1, to=5-4]
+			\arrow["{\bar{F}-\odot \bar{F}-}"', from=5-1, to=6-4]
+			\arrow["{\bar{F}}", from=5-4, to=6-4]
+		\end{tikzcd}
+	\end{equation*}
 \end{definition}
+\begin{remark}
+	Every horizontal lifting of a vertical endofunctor $F$ is an $\bar{F}$-double relator. Actually, these relators are highly well-behaved, and satisfy some of the mentioned properties of double relators. For example they are natural, normal (both are obvious) and symmetric.
+\end{remark}
+\begin{prop}
+	Every horizontal lifting is a symmetric double relator.
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+%\begin{definition}[Barr Double Relator]
+%	\todo{Finish}
+%\end{definition}
 \begin{example}
-	For a category $\BC_0$ with pullbacks, every Hermida-Jacobs bisimulation is an $\relar$-double coalgebra that $\relar$ is the map that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to a relation $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.
+	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}
 %
+\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:
+	\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
+	\end{gather*}
+\end{definition}
+%
+\begin{example}
+	We abstract Hughes-Jacobs simulation using poset-enrichment functor. On $\BC_1\rightrightarrows\BC_0$ with an endofunctor $F\c\BC_0\to\BC_0$ we have an $F$-double relator that takes every promorphism $\mathcal{R}$ to $P_FS\mathcal{R}\odot\mathcal{R}\odot P_FT\mathcal{R}$. More concretely, if $\BC_0$ is just an arbitrary category with pullbacks $\BC$, and $\BC_1=\rel(\BC)$ (it can also be $\spa(\BC)$ to give a different notion), then we have a double relator that takes $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{c_{PF_X}}{\leftarrow} P_FX\odot (FR)^\dagger\odot P_FY \stackrel{c_{PF_X}}{\to}Y)$.\todo{Check this!}
+\end{example}
+%
+\begin{prop}
+	Assuming that $\BC$ is a regular category with choice, then the concrete notion above is equivalent with Hermida-Jacobs simulation.
+\end{prop}
+\begin{proof}
+	\todo{Fisith!}
+\end{proof}
+%
+
 \todo{Talk more about the poset enrichment here. You can say that in $\rel(\BC)\rightrightarrows\BC$ and $\spa(\BC)\rightrightarrows\BC$ an order enrichment on $F$ can be represented as a functor of type $\BC\to\spa(\BC)$ or $\BC\to\rel(\BC)$!}
 \begin{definition}[Bi-laxed Barr Double Relator]
 	\todo{Finish}