bluh bluh

draft/draft.tex

@@ -3384,10 +3384,10 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 \end{proof}
 
 \begin{definition}[Mid-lax Barr relator]
-	Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$, and $\pi_1$ and $\pi_2$ are surjective, assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have:
+	Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$, and $\pi_1$ and $\pi_2$ are surjective, assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\relar$ is a \emph{mid-lax Barr relator} if we have:
 %	A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
 	\begin{gather*}
-		\overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op
+		\relar=F\pi_2\comp\appr\comp(F\pi_1)^\op
 	\end{gather*}
 \end{definition}
 
@@ -3533,17 +3533,20 @@ 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{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$.
+\end{notation}
 \begin{prop}\label{prop:lax-relator-full-comm}
 	For a functor $F$ with a liftable order we have:
 	\begin{gather*}
-		(\bar{F}r\comp\appr)\subseteq(\appr\comp\bar{F}r) 
+	F^\rightarrow r\leq F^\leftarrow r
 	\end{gather*}
 \end{prop}
 \begin{proof}
-	Assuming $x \mathrel{(\bar{F}r\comp\appr)} y$ and $\bar{F}r=F\pi_2\comp(F\pi_1)^\op$, then there exist $x'$ and $p$ such that $x\appr x'$, $p\mathrel{F\pi_1}x'$, and $p\mathrel{F\pi_2}y$. So, we have $x\appr F\pi_1(p)$ then by liftability there exists $p'$ such that $p'\appr p$, and $F\pi_1(p')=x$. Then from $p'\appr p$ we get $F\pi_2(p')\appr y$ that is equivalent with $p' \mathrel{(\appr\comp F\pi_2)} y$, and then we have $x \mathrel{(\appr\comp F\pi_2\comp(F\pi_1)^\op)} y$.\qed
+	Assuming $x \mathrel{(F^\rightarrow r)} y$ and $\bar{F}r=F\pi_2\comp(F\pi_1)^\op$, then there exist $x'$ and $p$ such that $x\appr x'$, $p\mathrel{F\pi_1}x'$, and $p\mathrel{F\pi_2}y$. So, we have $x\appr F\pi_1(p)$ then by liftability there exists $p'$ such that $p'\appr p$, and $F\pi_1(p')=x$. Then from $p'\appr p$ we get $F\pi_2(p')\appr y$ that is equivalent with $p' \mathrel{(\appr\comp F\pi_2)} y$, and then we have $x \mathrel{(\appr\comp F\pi_2\comp(F\pi_1)^\op)} y$ that is $x\mathrel{(F^\leftarrow r)}y$.\qed
 \end{proof}
 \begin{cor}
-	Assuming that $r$ is an $(\bar{F}r\comp\appr)$-simulation, then it is an $(\appr\comp\bar{F}r)$-simulation as well.
+	Assuming that $r$ is an $F^\rightarrow$-simulation, if $\appr$ is liftable, then it is an $F^\leftarrow$-simulation as well.
 \end{cor}
 %\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$.
@@ -3563,23 +3566,23 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	An $F$-relator $\relar$ is \emph{normal}, whenever for every set $X$, $\id_{FX}=\relar\id_X$.
 \end{definition}
 \begin{prop}
-	Every normal relational connect is difunctionally functorial.\qed
+	Every normal relational connector is difunctionally functorial.\qed
 \end{prop}
 
 \begin{prop}
-	Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. 
+	Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the relator $F^\leftarrow$ is natural. 
 \end{prop}
 \begin{proof}
 	\begin{align*}
-		\relar (g^\op\comp r\comp f)&\\
+		F^\leftarrow (g^\op\comp r\comp f)&\\
 		=&\appr\comp F(g^\op\comp r\comp f)\\
 		=&\appr\comp(Fg)^\op\comp Fr\comp Ff\\
 		=&(Fg)^\op\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\
-		=&(Fg)^\op\comp\relar r\comp Ff
+		=&(Fg)^\op\comp F^\leftarrow r\comp Ff
 	\end{align*}\qed
 \end{proof}
 \begin{remark}
-	One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning.
+	One may wonder if the above proposition is true for relators $F^\rightarrow$ or $F^\leftrightarrow$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning.
 \end{remark}
 \begin{prop}
 	Symmetrization of a natural relator, is natural.
@@ -3683,12 +3686,12 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \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!}
 %
-%\begin{prop}
-%	For every functor $F\c\Set\to\Set$, assuming $\relar$ is the left-lax Barr relator for $F$, then for every relation $r\subseteq X\times Y$, we have $\hat{\relar}r\subseteq \bar{F}r$.
-%\end{prop}
-%\begin{proof}
-%	
-%\end{proof}
+\begin{prop}\label{prop:left-lax-inc-triv}
+	For every functor $F\c\Set\to\Set$, we have $\bar{F}\leq F^\leftarrow$.
+\end{prop}
+\begin{proof}
+	For a relation $r$, assuming $(x,y)\in \bar{F}r$, since $\appr$ is reflexive we have $y\mathrel{\appr}y$, so we have $x\mathrel{(\bar{F}\comp\appr)} y$ that is $(x,y)\in F^\leftarrow r$.\qed 
+\end{proof}
 %
 \subsection{Symmetric relation}
 \begin{prop}
@@ -3706,7 +3709,7 @@ Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a
 	Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed
 \end{proof}
 \begin{cor}
-	For a functor $F\c\Set\to\Set$, assuming that for a relation $r$ we have $\appr\comp\bar{F}r\leq\bar{F}r$, if $r$ is symmetric, and it is a $\appr\comp\bar{F}$-simulation, then it is a $\hat{\appr\comp\bar{F}}$-bisimulation.\ppnote{This is a bad notation for lax Barr-relators. Switch them with $F^\rightarrow$, $F^\leftarrow$, and $F^\leftrightarrow$.}
+	Recalling~\autoref{prop:left-lax-inc-triv}, for a functor $F\c\Set\to\Set$, assuming that $F^\leftarrow\leq\bar{F}$, we get $F^\leftarrow=\bar{F}$. So, if $r$ is symmetric, and it is a $F^\leftarrow$-simulation, then it is a $\bar{F}$-bisimulation.
 \end{cor}
 \end{document}