a prop

draft/draft.tex

@@ -3191,13 +3191,13 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i
 	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:
+	For a functor $F$ with a liftable order we have:
 	\begin{gather*}
-		\bar{F}r\comp\appr=\appr\comp\bar{F}
+		(\bar{F}r\comp\appr)\subseteq(\appr\comp\bar{F}r) 
 	\end{gather*}
 \end{prop}
 \begin{proof}
-	\todo{Write it down. You have it in your notes.}
+	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
 \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$.