Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

draft/draft.tex

@@ -2171,7 +2171,24 @@ We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined
 		\{1,2\} & x=1  \\
 		\{2,3\} & x=2\\
 		\{3\} & x=3
-	\end{cases}
+	\end{cases}\qquad
+\begin{tikzpicture}[scale=0.1]
+	\tikzstyle{every node}+=[inner sep=0pt]
+	\draw [black] (23.8,-25.2) circle (3);
+	\draw (23.8,-25.2) node {$1$};
+	\draw [black] (42.4,-25.2) circle (3);
+	\draw (42.4,-25.2) node {$2$};
+	\draw [black] (33,-34.6) circle (3);
+	\draw (33,-34.6) node {$3$};
+	\draw [black] (22.477,-22.52) arc (234:-54:2.25);
+	\fill [black] (25.12,-22.52) -- (26,-22.17) -- (25.19,-21.58);
+	\draw [black] (41.077,-22.52) arc (234:-54:2.25);
+	\fill [black] (43.72,-22.52) -- (44.6,-22.17) -- (43.79,-21.58);
+	\draw [black] (26.8,-25.2) -- (39.4,-25.2);
+	\fill [black] (39.4,-25.2) -- (38.6,-24.7) -- (38.6,-25.7);
+	\draw [black] (40.28,-27.32) -- (35.12,-32.48);
+	\fill [black] (35.12,-32.48) -- (36.04,-32.27) -- (35.33,-31.56);
+\end{tikzpicture}
 \end{gather*}
 $\sigma$ is defined as below:
 \begin{gather*}
@@ -3137,6 +3154,15 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \begin{proof}
 	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{prop}\label{prop:lax-relator-full-comm}
+	Assuming the axiom of choice, for a functor $F$ with a liftable order we have:
+	\begin{gather*}
+		\bar{F}r\comp\appr=\appr\comp\bar{F}
+	\end{gather*}
+\end{prop}
+\begin{proof}
+	\todo{Write it down. You have it in your notes.}
+\end{proof}
 %\begin{example}
 %	In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$.
 %	
@@ -3258,7 +3284,22 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{remark}
 	With a similar argument we can prove that the symmetrization of a right-lax Barr-relator of $F$ is a Barr-relator.
 \end{remark}
-\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion.}
+\begin{lemma}\label{lem:lax-relator-str}
+	For a relation $r$, for functions $k_s\c F\pi_1(\bar{F}r)\to\powf FX$ and $k_b\c F\pi_2(\bar{F}r)\to\powf FX$, defined as 
+	\begin{gather*}
+		k_s(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x'\appr x, (x',y)\notin\bar{F}r\},\\
+		k_b(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x\appr x', (x',y)\notin\bar{F}r\},
+	\end{gather*}
+	we have
+	\begin{gather*}
+		(\bar{F}r)\comp\appr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_s(x)),\\
+		(\bar{F}r)\comp\sappr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_b(x)).
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	\todo{Write it down. You have it in your notes.}
+\end{proof}
+\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!}
 \end{document}