moreo

draft/draft.tex

@@ -1940,36 +1940,36 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 \end{definition}
  
 \begin{definition}[Hermida-Jacobs Simulation]
-	For a relator $\relar$ on 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$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
+	For a relator $\relar$ on a functor $F$ a HJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
 	\begin{equation*}\label{def:hej-sim}
 		\begin{tikzcd}[ampersand replacement=\&]
 			X \& r \& Y \\
-			{FX} \& {\appr;\relar r;\appr} \& {FY}
+			{FX} \& {\relar r} \& {FY}
 			\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["\beta", from=1-3, to=2-3]
-			\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
-			\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
+			\arrow["{{(Fp_1)}^\relar}", from=2-2, to=2-1]
+			\arrow["{{(Fp_2)}^\relar}"', from=2-2, to=2-3]
 		\end{tikzcd}
 	\end{equation*}
 \end{definition}
-\begin{prop}
-	Hughes-Jacobs simulation is an instance of HJ-simulation, where $\relar r=(Fr)^\dagger$. 
-\end{prop}
-\begin{proof}
-	We need to show that $(F-)^\dagger$ is a relator. We need to show that for a relations $r_1$ and $r_2$, where $r_1\appr r_2$ we have $\relar r_1\appr \relar r_2$. (What is $\appr$?!) 
-	
-	\todo{Sergey claims this. Ask him how can he?}
-\end{proof}
 \begin{prop}
 	For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique.
 \end{prop}
 \begin{proof}
-	It only relies on the fact that ${Fp_1}_\appr$ and ${Fp_2}_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed
+	It only relies on the fact that ${(Fp_1)}^\relar_\appr$ and ${(Fp_2)}^\relar_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed
 \end{proof}
-
+\begin{definition}
+	We call $\hat{\relar}$ a symmetrization of a relator $\relar$ iff for a relation $r$ it is defined as follows:
+	\begin{gather*}
+		\hat{\relar}r=\relar r\cap (\relar(r^\op))^\op
+	\end{gather*}
+\end{definition}
+\begin{prop}
+	Assuming that $\relar$ is a relator, and $r$ is a symmetric relation that is a simulation for $\relar$, then $r$ is also a simulation for $\hat{\relar}$.
+\end{prop}
 \end{document}