minor

draft/draft.tex

@@ -1346,7 +1346,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 	\label{fig:bisim-choice}
 \end{figure}
 \section{Coalgebraic Simulation}
-\todo{Give an introduction of the definitions for $\spa(\BC)$ and $\rel(\BC)$ that are AM-simulation and HJ-simulation, then open up the discussion about relators.}
+%\todo{Give an introduction of the definitions for $\spa(\BC)$ and $\rel(\BC)$ that are AM-simulation and HJ-simulation, then open up the discussion about relators.}
 \begin{definition}[Aczel-Mendler Simulation]
 	Assuming that $\appr$ is a natural order structure on a functor $F\c\BC\to\BC$, an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\spa(\BC)$ is an \emph{Aczel-Mendler simulation} from a coalgebra $(X,\alpha)$ to $(Y,\beta)$, whenever the following diagram commutes laxly:
 	\begin{equation}\label{eq:diag-am-sim}
@@ -1410,7 +1410,7 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 %	($\Leftarrow$): If $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an object in $\rel$, then $R$ is a binary relation from $X$ to $Y$ so, it is a morphism of type $X\rto Y$ in $\rels$.\qed
 %\end{proof}
 %The above translation seems to be true in a more general case, where $\spa$ and $\rel$ are defined on an arbitrary category (the latter is called an allegory then).
-\begin{definition}[Relator]
+\begin{definition}[Relator]\label{def:relator}
 	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\Rel$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$. 
 \end{definition}
 %
@@ -1967,19 +1967,22 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 \begin{definition}[Double Relator]
 	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 F=\relar\comp S$
-		\item $T\comp F=\relar\comp T$
+		\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}
 \begin{remark}
-	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 morphism, 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 preserve identities and compositions.
+	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}[Double Coalgebra]
-	Given a double category $\BC_1\rightrightarrows\BC_0$, and a $F$-double relator $\relar$, a pair $(\mathcal{R},\delta)$ is an $\relar$-double coalgebra on $\BC_1\rightrightarrows\BC_0$.
+	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}
 \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.}
 \section{Symmetric Simulation is a Bisimulation}