pc sync

draft/draft.tex

@@ -2163,8 +2163,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %	We have $(Fp_1)^\dagger\comp\sigma$.
 %\end{proof}
 \begin{example}
-And another counter-example!!! 
-Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. We show the functor with $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
+Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. Let us call this functor $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
 We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
 \begin{gather*}
 	\alpha(x)=
@@ -3213,7 +3212,7 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	\end{align*}\qed
 \end{proof}
 \begin{cor}
-	Since the symmetrization of left-lax Barr relator that is laxed with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
+	Since the symmetrization of left-lax Barr relator with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
 \end{cor}
 \begin{cor}
 	By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well.