def

draft/draft.tex

@@ -286,6 +286,8 @@
 \newcommand{\rel}{\mathbf{Rel}}
 \newcommand{\gra}{\mathbf{Gra}}
 \newcommand{\obj}{\mathbf{Obj}}
+\newcommand{\relar}{\mathbf{R}}
+\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
 
 \newcommand{\simeet}{%
 	\mathbin{%
@@ -1817,8 +1819,16 @@ Abstractly, first we define an operation that we need on morphisms that takes tw
 \begin{lemma}\label{lem:alph-prod-abs}
 	Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation witnesses of the type $R\to (FR)^\dagger$, then there exists a simulation witness $\sigma\in S$ that,  $(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1$. 
 \end{lemma}
+\begin{proof}
+	Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ as the following:
+	\begin{gather*}
+		\sigma=\brks{(\alpha\comp p_1), (Fp_2)^\dagger\comp\delta}
+	\end{gather*}
+	We have $(Fp_1)^\dagger\comp\sigma$.
+\end{proof}
 \section{Relators}
-We start the discussion with answering the question that why there can be multiple simulation structures based on~\autoref{def:sim}.
+In this section we want to discuss relators. We set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
+We answer the question that why there can be multiple simulation structures based on~\autoref{def:sim}.
 At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
@@ -1878,69 +1888,26 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 	u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
 	u(\inr w)=w
 \end{gather*}
-Now, we want to prove a more abstract version of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram:
-\begin{equation*}
-	\begin{tikzcd}[ampersand replacement=\&]
-		{\appr;(FR)^\dagger;\appr} \& {\appr;(FR)^\dagger} \& {\appr} \& {FX} \\
-		\& (FR)^\dagger \& {FX} \\
-		{\appr} \& {FX} \\
-		{FX}
-		\arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2]
-		\arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-2]
-		\arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3]
-		\arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2]
-		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
-		\arrow["{{{{{{{q_1}}}}}}}", from=1-3, to=1-4]
-		\arrow["{{{{{{{q_2}}}}}}}", from=1-3, to=2-3]
-		\arrow["{{{{{{{Fp_1^\dagger}}}}}}}", from=2-2, to=2-3]
-		\arrow["{{{{{{{Fp_2^\dagger}}}}}}}"', from=2-2, to=3-2]
-		\arrow["{{{{{{{q_1}}}}}}}"', from=3-1, to=3-2]
-		\arrow["{{{{{{{q_2}}}}}}}"', from=3-1, to=4-1]
-	\end{tikzcd}
-\end{equation*}
-Additionally, we make the abbreviations that ${Fp_1}_\appr=q_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=q_2\comp\pi_2$.
-\begin{prop}
-	Assuming we have a morphism $\sigma'\c R\to(FR)^\dagger$ then exists $\delta\c(FR)^\dagger\to(\appr;(FR)^\dagger;\appr)^\dagger$ such that $\sigma=\delta\comp\sigma'$ that commutes in the following diagram:
+\begin{definition}[Relator]
+	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends a morphism of $\Rel$ that is a relation $X\rto Y$ to $FX\rto FY$. 
+\end{definition}
+ 
+\begin{definition}[Hermida-Jacobs Simulation]
+	For a relator $\relar$ for a functor $F$, and a poset $\appr$ over $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ such that the following diagram commutes ($;$ is the relation composition):
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			X \& R \& X \\
-			{FX} \& {(FR)^\dagger} \& {FX} \\
-			{FX} \& {(\appr;(FR)^\dagger;\appr)^\dagger} \& {FX}
+			{FX} \& {\appr;(FR)^\dagger;\appr} \& {FX}
 			\arrow["\alpha"', from=1-1, to=2-1]
 			\arrow["{p_1}"', from=1-2, to=1-1]
 			\arrow["{p_2}", from=1-2, to=1-3]
-			\arrow["{\sigma'}", from=1-2, to=2-2]
+			\arrow["\sigma", from=1-2, to=2-2]
 			\arrow["\alpha", from=1-3, to=2-3]
-			\arrow["id"', from=2-1, to=3-1]
-			\arrow["\delta", from=2-2, to=3-2]
-			\arrow["id"', from=2-3, to=3-3]
-			\arrow["{({Fp_1}_\appr)^\dagger}", from=3-2, to=3-1]
-			\arrow["{({Fp_2}_\appr)^\dagger}"', from=3-2, to=3-3]
+			\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
+			\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
 		\end{tikzcd}
 	\end{equation*}
-\end{prop}
-\begin{proof}
-	Ultimately, we need to define $\delta'\c(FR)\to\appr;(FR)^\dagger;\appr$, where $\delta=e_{\appr;(FR)^\dagger;\appr}\comp\delta'$, and $e_{\appr;(FR)^\dagger;\appr}\c\appr;(FR)^\dagger;\appr\to(\appr;(FR)^\dagger;\appr)^\dagger$ is the epimorphism in the epi-mono factorization of $\brks{{Fp_1}_\appr,{Fp_2}_\appr}$ because by~\autoref{lem:norm-simp} it suffices to show that the following diagram commutes:
-	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
-			X \& R \& X \\
-			FX \& {(FR)^\dagger} \& FX \\
-			FX \& {\appr;(FR)^\dagger;\appr} \& FX
-			\arrow["\alpha"', from=1-1, to=2-1]
-			\arrow["{{p_1}}"', from=1-2, to=1-1]
-			\arrow["{{p_2}}", from=1-2, to=1-3]
-			\arrow["{{\sigma'}}", from=1-2, to=2-2]
-			\arrow["\alpha", from=1-3, to=2-3]
-			\arrow["id"', from=2-1, to=3-1]
-			\arrow["{\delta'}", from=2-2, to=3-2]
-			\arrow["id"', from=2-3, to=3-3]
-			\arrow["{{{Fp_1}_\appr}}", from=3-2, to=3-1]
-			\arrow["{{{Fp_2}_\appr}}"', from=3-2, to=3-3]
-		\end{tikzcd}
-	\end{equation*}
-	So, we need to define $\delta'$.
-\end{proof}
+\end{definition}
 \end{document}