more double category

draft/draft.tex

@@ -1439,6 +1439,10 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 	A relator $\relar$ is symmetric if and only if for every relation $R$ we have $\relar(R^\op)=(\relar R)^\op$.
 \end{definition}
 %
+\begin{definition}[Natural Relator]
+	An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$, and arbitrary functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp R\comp f)=(Fg)^\op\comp\relar R\comp Ff$.
+\end{definition}
+%
 \begin{definition}[Relator-based Bisimulation]
 	Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-bisimulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ whenever $R$ is an $\relar$-simulation, and $\relar$ is a symmetric relator.
 \end{definition}
@@ -1957,19 +1961,14 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 %\subsection{Choosing a suitable order for our setting}
 %Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
 \section{Simulations and Bisimulations in Double Categories}
-\subsection{Bisimulation in Double Categories}
-\todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".}
-\subsection{Simulations in Double Categories}
-\todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!}
 %
 %
 %
-\begin{definition}[Double Relator]
+\begin{definition}[Double Relator]\label{def:doub-rela}
 	Given a double category $\BC_1\rightrightarrows\BC_0$, for an endofunctor $F$, an $F$-double relator $\relar$ is an endomap on objects and morphisms of category $\BC_1$, for which the following equations hold:
 	\begin{enumerate}
 		\item $S\comp\relar=F\comp S$
 		\item $T\comp\relar=F\comp T$
-		\item $\relar\comp U=U\comp F$
 	\end{enumerate}
 	Additionally, it takes every cell of type $\mathcal{R}\Rightarrow\mathcal{S}$ to a cell of type $\relar\mathcal{R}\Rightarrow\relar\mathcal{S}$.
 \end{definition}
@@ -1977,14 +1976,39 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 	In the above definition we are describing an endomap on objects and morphisms of a category, and we form equations with compositions of this map. The composition that we mean, is the one over functions and not the functors. Indeed, it does not make a functor, but it makes another function. Additionally, the endomap that we define is actually two endomaps on objects and morphisms, respectively, but we use the tradition in denoting functors for it that is to use one letter to refer to both maps. Basically, one can think of a relator $\relar$ as a functor that does not necessarily preserve identities and compositions.
 \end{remark}
 %
+\begin{definition}[Normal Double Relator]
+	A $F$-double relator $\relar$ is normal, whenever the following equation holds:
+	\begin{gather*}
+			\relar\comp U=U\comp F
+	\end{gather*} 
+\end{definition}
 \begin{definition}[Double Coalgebra]
 	Given a double category $\BC_1\rightrightarrows\BC_0$, and a $F$-double relator $\relar$, a pair $(\mathcal{R},\delta)$ that $\delta\c\mathcal{R}\Rightarrow\relar\mathcal{R}$ is an $\relar$-double coalgebra on $\BC_1\rightrightarrows\BC_0$.
 \end{definition}
-\begin{example}
-	Every relator defined 
-\end{example}
+%
+	Given an $F$-relator $\relar$ defined in~\autoref{def:relator} we have a canonical way to extend its definition over morphisms of $\rel_a$ as well:
+\begin{definition}[Extendable Relator]
+	Assuming $\relar$ is an $F$-relator, it is an \emph{extendable} relator whenever for every morphims $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ there exists the morphism $(Fg_1,Fg_2)\c(FX_1 \stackrel{Fp_1}{\leftarrow} \relar R \stackrel{Fp_2}{\to}FX_2)\to(FY_1 \stackrel{Fq_1}{\leftarrow} \relar S \stackrel{Fq_2}{\to}FY_2)$ in $\rel_a$.
+\end{definition}
+%
+	It is obvious that every extendable relator is a double relator in $\rel_a\rightrightarrows\Set$ and vice-versa.
+%
+\begin{prop}
+	Every natural $F$-relator $\relar$ is extendable.
+\end{prop}
+\begin{proof}
+	Assuming that there exists $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ we need to show that exists the morphism $(Fg_1,Fg_2)\c(FX_1 \stackrel{Fp_1}{\leftarrow} \relar R \stackrel{Fp_2}{\to}FX_2)\to(FY_1 \stackrel{Fq_1}{\leftarrow} \relar S \stackrel{Fq_2}{\to}FY_2)$ in $\rel_a$. It is equivalent with showing that $\relar R\subseteq (Fg_2)^\op\comp\relar S\comp Fg_1$. Since $\relar$ is natural we have $(Fg_2)^\op\comp\relar S\comp Fg_1=\relar(g_2^\op\comp S\comp g_1)$. Existence of $(g_1,g_2)$ is equivalent with $R\subseteq g_2^\op\comp S\comp g_1$, so by the monotonicity of $\relar$ as a relator we have $\relar R\subseteq \relar(g_2^\op\comp S\comp g_1)$. So, we have $\relar R\subseteq Fg_2^\op\comp \relar S\comp Fg_1$.\qed
+\end{proof}
+\begin{cor}
+	Every natural relator is a double relator in $\rel_a\rightrightarrows\Set$.
+\end{cor}
+So, now we see that for every natural relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-simulation from a coalgebra $(X,f)$ to $(Y,g)$ if and only if $((X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y),(f,g))$ is an $\relar$-double coalgebra in $\rel_a\rightrightarrows\Set$.
 \todo{First, finish the subsection in section 2, then come back here and continue this by saying that every relator is a double relator in $\Set$, and then define symmetric double relators, and then instantiate every notion that you have introduced in previous sections.}
 \todo{Perhaps in the future you can also introduce properties of relators for double relatros.}
+\subsection{Bisimulation in Double Categories}
+\todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".}
+\subsection{Simulations in Double Categories}
+\todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!}
 \section{Symmetric Simulation is a Bisimulation}
 \todo{Obviously, this chapter should be changed. All the definitions should be moved to somewhere else. You should start the chapter by giving your counter examples, and then presenting your proofs.}
 \begin{definition}[Graph]