bluh

draft/draft.tex

@@ -283,6 +283,7 @@
 \newcommand{\refl}{\mathsf{refl}}
 \newcommand{\trans}{\mathsf{trans}}
 \newcommand{\preord}{\mathbf{PreOrd}}
+\newcommand{\poset}{\mathbf{PoSet}}
 \newcommand{\rel}{\mathbf{Rel}}
 \newcommand{\spa}{\mathbf{Span}}
 \newcommand{\gra}{\mathbf{Gra}}
@@ -398,9 +399,9 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}}
 		\item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II}
 	\end{enumerate}
 \end{definition}
-We want to say that a natural order structure entails an order over a functor defined by Jacobs and Hughes that is a functor of the type $\Set\to\mathbf{Poset}$.
+We want to say that a natural order structure entails an order over a functor defined by Jacobs and Hughes that is a functor of the type $\Set\to\poset$.
 \begin{prop}
-	Assuming that $F\c\Set\to\Set$ is a functor, and we have a natural order structure on $F$, then we have a functor $\tilde{F}\c\Set\to\mathbf{Poset}$, such that $U\comp \tilde{F}=F$, where $U$ is a forgetful functor.
+	Assuming that $F\c\Set\to\Set$ is a functor, and we have a natural order structure on $F$, then we have a functor $\tilde{F}\c\Set\to\poset$, such that $U\comp \tilde{F}=F$, where $U$ is a forgetful functor.
 \end{prop}
 \begin{proof}
 	We take $\tilde{F}X=\Hom(1,FX)$. Assuming that $U$ takes every poset to its carrier set, then we have $U\comp\tilde{F}X=FX$ for every object $X$.\qed
@@ -1067,20 +1068,23 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 \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".}
 %
+\section{Spans and Relations with Lax Morphisms}
+\todo{Finish!}
 \section{Coalgebraic Simulation}
-We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.
-\begin{definition}[A Preorder Over a Functor]
-	Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes:
-	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
-			\& \preord \\
-			\Set \& \Set
-			\arrow[from=1-2, to=2-2]
-			\arrow["\appr", from=2-1, to=1-2]
-			\arrow["F"', from=2-1, to=2-2]
-		\end{tikzcd}
-	\end{equation*}
-\end{definition}
+\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.}
+%We show the category of partially ordered sets with monotone functions between them with $\poset$. 
+%\begin{definition}[A Partial Order Over a Functor]
+%	Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes:
+%	\begin{equation*}
+%		\begin{tikzcd}[ampersand replacement=\&]
+%			\& \preord \\
+%			\Set \& \Set
+%			\arrow["U", from=1-2, to=2-2]
+%			\arrow["\appr", from=2-1, to=1-2]
+%			\arrow["F"', from=2-1, to=2-2]
+%		\end{tikzcd}
+%	\end{equation*}
+%\end{definition}
 %
 %
 %We gave an introduction to Hughes and Jacobs paper. They also have a way to represent simulation relations. In the following, we try to find a suitable formalization for simulation relations, inspired by Hughes and Jacobs.