more editting

draft/draft.tex

@@ -103,6 +103,7 @@
 \usepackage{proof}
 \usepackage{xspace}
 \usepackage{bm}
+\usepackage{pifont}
 
 \input{catprog}
 
@@ -705,7 +706,7 @@ From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$
 \begin{gather*}
 	(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
 \end{gather*}
-From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to show the categories of spans and relations with onymous morphisms.
+From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to denote the categories of spans and relations with onymous morphisms.
 \begin{prop}\label{prop:rel-rela}
 	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\rel_a$, there is a morphism $(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$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness $w\c R\to S$.
 \end{prop}
@@ -714,7 +715,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
 	\begin{align*}
 		g_1\comp p_1(x_1,x_2)&\\
 		=&g_1(x_1)\\
-		=&q_1(g(x_1),g(x_2))\\
+		=&q_1(g_1(x_1),g_2(x_2))\\
 		=&q_1\comp w(x_1,x_2)
 	\end{align*}
 	Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
@@ -726,7 +727,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
 	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\spa$ and $\spa_a$, there is a morphism $(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 $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
-	($\Rightarrow$): We need the axiom of choice to prove this statement. By the definition of anonymous morphisms, for every $u\in R$ there exists $v\in S$ such that $q_1(v)=p_1\comp g_1(u)$ and $q_2(v)=p_2\comp g_2(u)$. So, for each $u\in R$ there exists a set $V_u\in\powf S$ that its elements have the mentioned properties. We can form a function $h\c R\to \powf S$ that $h(u)=V_u$. The image of $h$ that we show with $\im(h)$ is a family of non-empty sets. By the axiom of choice, there exists a function $s\c \im(h)\to S$. We define $w\c R\to S$ as $w=s\comp h$, then for every $u\in R$, we have $q_1\comp w(u)=g_1\comp p_1(u)$ and $q_2\comp w(u)=g_2\comp p_2(u)$.
+	($\Rightarrow$): We need the axiom of choice to prove this statement. By the definition of anonymous morphisms, for every $u\in R$ there exists $v\in S$ such that $q_1(v)=p_1\comp g_1(u)$ and $q_2(v)=p_2\comp g_2(u)$. So, for each $u\in R$ there exists a set $V_u\in\powf S$ that its elements have the mentioned properties. We can form a function $h\c R\to \powf S$ that $h(u)=V_u$. The image of $h$ that we denote with $\im(h)$ is a family of non-empty sets. By the axiom of choice, there exists a function $s\c \im(h)\to S$. We define $w\c R\to S$ as $w=s\comp h$, then for every $u\in R$, we have $q_1\comp w(u)=g_1\comp p_1(u)$ and $q_2\comp w(u)=g_2\comp p_2(u)$.
 	
 	($\Leftarrow$): Assuming $u\in R$, there exists $w(u)\in S$, and by the definition of onymous morphisms we have $q_1(w(u))=g_1\comp p_1(u)$ and $q_2(w(u))=g_2\comp p_2(u)$. \qed
 \end{proof}
@@ -746,7 +747,24 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
 \begin{proof}
 	Trivial by the definitions.\qed
 \end{proof}
-
+\begin{figure}[t]
+	\centering
+	\begin{tabular}{|l|c|c|c|c|}
+		\hline
+		\quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\
+		\hline
+		$\spa$ &  & & & \\
+		\hline
+		$\rel$ & & & & \\
+		\hline
+		$\spa_a$ & \ding{56} & & & \\
+		\hline
+		$\rel_a$ & & & & \\
+		\hline
+	\end{tabular}
+	\caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column exists, in $\Set$.}
+	\label{fig:anonymous_onymous-choice}
+\end{figure}
 %\begin{notation}
 %	In the literature it is common to see a category that has sets as objects, and binary relations as morphims. Here we denote this category $\rel'$.
 %\end{notation}
@@ -1169,7 +1187,7 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta
 \end{definition}
 %
 \begin{definition}[Relation Lifting]
-	Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
+	Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, whenever the following diagram commutes:
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			\rel(\BC) \&\& \rel(\BC) \\
@@ -1200,14 +1218,14 @@ The given definition is highly abstract. There is a relation lifting that abstra
 	
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
-			R \& {R^\dagger} \&\& {X\times Y}
+			R \& {R^\clubsuit} \&\& {X\times Y}
 			\arrow["{e_R}"', two heads, from=1-1, to=1-2]
 			\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
-			\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
+			\arrow["{\brks{p^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4]
 		\end{tikzcd}
 	\end{equation*}
-	Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we show it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
+	Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
-	So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
+	So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			\& {(FR)^\dagger} \& \\
@@ -1287,7 +1305,9 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 	
 	(2): Follows from~\autoref{prop:rel-rela}.
 	
-	(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\qed
+	(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\\
+	($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $(x,y)\in R$ there then $(\alpha(x),\beta(y))\in(FR)^\dagger$ that means that exists $u\in FR$ such that $Fp_1(u)=\alpha(x)$ and $Fp_2(u)=\beta(u)$, and it exactly means that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation.
+	\qed
 \end{proof}
 \begin{cor}
 	Recalling~\autoref{prop:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice.
@@ -1307,6 +1327,24 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 	\label{fig:anonymous_onymous}
 \end{figure}
 %
+\begin{figure}[t]
+	\centering
+	\begin{tabular}{|l|c|c|c|c|}
+		\hline
+		\qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\
+		\hline
+		Aczel-Mendler &  & & & \\
+		\hline
+		Hermida-Jacobs & \ding{56} & & & \\
+		\hline
+		Span-based & \ding{56} & & & \\
+		\hline
+		Hughes-Jacobs & \ding{56} & & & \\
+		\hline
+	\end{tabular}
+	\caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.}
+	\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.}
 \begin{definition}[Aczel-Mendler Simulation]
@@ -1428,6 +1466,39 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 	The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.
 \end{rem}
 Having lax versions of a symmetric relator, allows us to have simulation relations that are related to bisimulation. Also, we did show in the previous proposition that making the commuting diagram lax, with the relator that is not laxed, we get an equivalent definition under the axiom of choice. But if the relator is not symmetric, it is already giving us a notion of simulation, even though we have not laxed it!
+%\begin{figure}[t]
+%	\centering
+%	\begin{tabular}{|l|c|c|}
+%		\hline
+%		& \textbf{Anonymous} & \textbf{Onymous} \\
+%		\hline
+%		\textbf{Relations} & Hughes-Jacobs & Hermida-Jacobs \\
+%		\hline
+%		\textbf{Spans} & Span-based & Aczel-Mendler \\
+%		\hline
+%	\end{tabular}
+%	\caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.}
+%	\label{fig:anonymous_onymous-sim}
+%\end{figure}
+%\begin{figure}[t]
+%	\centering
+%	\begin{tabular}{|l|c|c|c|c|}
+%		\hline
+%		\qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\
+%		\hline
+%		Aczel-Mendler &  & & & \\
+%		\hline
+%		Hermida-Jacobs & \ding{56} & & & \\
+%		\hline
+%		Span-based & \ding{56} & & & \\
+%		\hline
+%		Hughes-Jacobs & \ding{56} & & & \\
+%		\hline
+%	\end{tabular}
+%	\caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.}
+%	\label{fig:sim-choice}
+%\end{figure}
+%
 %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:
@@ -1923,7 +1994,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 			\arrow["{p_2}", from=1-2, to=2-3]
 		\end{tikzcd}
 	\end{equation*}
-	Graphs over $\BC$ form a category that we show by $\gra(\BC)$.
+	Graphs over $\BC$ form a category that we denote by $\gra(\BC)$.
 \end{definition}
 \begin{definition}[Symmetric Graph]
 	A graph $(R,X)$ is symmetric iff there exists an endomorphism $s\c R\to R$, such that the following diagram commutes
@@ -1946,7 +2017,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 	Symmetry of a graphs over preserved a functor.
 \end{lemma}
 \begin{definition}[Relation]
-	A relation in a category $\BC$ is a graph $(R,X)$ where $\brks{p_1,p_2}\c R \to X\times Y$ is monic. Relations over $\BC$ form a category that we show by $\rel(\BC)$.
+	A relation in a category $\BC$ is a graph $(R,X)$ where $\brks{p_1,p_2}\c R \to X\times Y$ is monic. Relations over $\BC$ form a category that we denote by $\rel(\BC)$.
 \end{definition}
 \begin{definition}[Jointly Monic]
 	A pair of morphisms $p_1,p_2\c R\to X$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$.
@@ -2051,7 +2122,7 @@ We can define $(-)^\dagger$ as a functor from $\gra(\BC)\to\rel(\BC)$, then we d
 	\end{equation*}
 	\qed
 \end{proof}
-We show this relation with $F_\rel(R,X)$.
+We denote this relation with $F_\rel(R,X)$.
 \begin{definition}[Simulation]\label{def:sim}
 	A coalgebra $\sigma\c R\to (FR)^\dagger$ is a simulation over the $F$-coalgebra $\alpha\c X\to FX$ iff the following diagram is lax-commutative:
 	\begin{equation}\label{eq:diag-lax-sim}
@@ -3507,13 +3578,13 @@ To define $\delta$, we define $c\c(\powf R^\dagger)\to((\powf R^\dagger)\times R
 \end{gather*}
 \subsection{Symmetric simulation}
 \begin{notation}
-	From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$. Also, we show the category of relations over set that we represent by spans with $\spa$, and $\rel$ is the category of sets and binary relations between them.
+	From now on, we denote relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$. Also, we denote the category of relations over set that we represent by spans with $\spa$, and $\rel$ is the category of sets and binary relations between them.
 \end{notation}
 \begin{lemma}\label{lem:rel-span-equiv}
 	$r\c X\rto Y$ is a morphism in $\rel$ iff there is an object $(r,p_1,p_2)$ in $\spa$.
 \end{lemma}
 \begin{proof}
-	($\Rightarrow$): $r\c X\rto Y$ being a morphism in $\rel$ means that in $\Set$ there exist an object $r$ with a unique mono of type $r\to X\times Y$ that is a pairing that we show with $\brks{p_1,p_2}$. So, $(r,p_1,p_2)$ form an object in $\spa$.
+	($\Rightarrow$): $r\c X\rto Y$ being a morphism in $\rel$ means that in $\Set$ there exist an object $r$ with a unique mono of type $r\to X\times Y$ that is a pairing that we denote with $\brks{p_1,p_2}$. So, $(r,p_1,p_2)$ form an object in $\spa$.
 	
 	($\Leftarrow$): If $(r,p_1,p_2)$ is an object in $\spa$, then $r$ is a binary relation from $X$ to $Y$ so, it is a morphism of type $X\rto Y$ in $\rel$.\qed
 \end{proof}
@@ -3688,7 +3759,7 @@ then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in
 	Assuming that $\relar$-similarity is symmetric and complete, then $\hat{\relar}$-similarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete.
 \end{prop}
 \begin{proof}
-	(Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since  
+	(Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behavioural equivalence with $r_b$. Since  
 \end{proof}
 
 \begin{prop}
@@ -3943,7 +4014,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
 \end{proof}
 \begin{notation}
-	From now on we show relators $\bar{F}-\comp\appr$ with $F^\rightarrow$, $\appr\comp\bar{F}-$ with $F^\leftarrow$, and $\appr\comp\bar{F}-\comp\appr$ with $F^\leftrightarrow$.
+	From now on we denote relators $\bar{F}-\comp\appr$ with $F^\rightarrow$, $\appr\comp\bar{F}-$ with $F^\leftarrow$, and $\appr\comp\bar{F}-\comp\appr$ with $F^\leftrightarrow$.
 \end{notation}
 \begin{prop}\label{prop:lax-relator-full-comm}
 	For a functor $F$ with a liftable order we have:
@@ -4022,7 +4093,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal.
 \end{prop}
 \begin{proof}
-	We show the left-lax Barr relator with $\relar$. We have:
+	We denote the left-lax Barr relator with $\relar$. We have:
 	\begin{align*}
 		\hat{\relar}\id&\\
 		=&\relar\id\cap(\relar\id^\op)^\op\\