prop

draft/draft.tex

@@ -2205,9 +2205,17 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 		\item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
 	\end{itemize}
 \end{proof}
-\begin{remark}
+\begin{lemma}\label{lem:maybe-colif}
-	The mentioned order on the maybe functor is not coliftable.
+	The order structure on the set-functor $FX=X+1$ is a liftable order.
-\end{remark}
+\end{lemma}
+\begin{proof}
+	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $Fg(k)\appr h$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k\appr k'$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
+	\begin{itemize}
+		\item $Fg(k)=h$: In this case we take $k'=k$, and then we have $Fg(k')=h$.
+		
+		\item $Fg(k)=\bot$: It entails that $k=\bot$. We either have $h=\bot$ or $h\in Y$. If $h=\bot$ then we take $k'=k$, and we are done. If $h\in Y$, then by the surjectivity of $g$, there exists $k'$ such that $g(k')=h$ that entails $Fg(k')=h$ as well.\qed
+	\end{itemize}
+\end{proof}
 So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$.
 \begin{lemma}\label{lem:maybe-func-set}
 	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ 
@@ -3041,6 +3049,30 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \begin{proof}
 	\todo{Finish.}
 \end{proof}
+\begin{lemma}
+	The non-trivial order on the maybe functor $FX=X+1$ is a liftable order.
+\end{lemma}
+\begin{prop}
+	Assuming $F$ is the maybe functor $FX=X+1$, then the syemmetrization of the left-lax Barr relator of $F$ is a Barr-relator.
+\end{prop}
+\begin{proof}
+	We have the following:
+	\begin{align*}
+		\appr\comp\bar{F}r\cap(\appr\comp\bar{F}r^\op)^\op&\\
+		=&\appr\comp\bar{F}r\cap(\appr\comp F\pi_1\comp(F\pi_2)^\op)^\op\\
+		=&\appr\comp\bar{F}r\cap F\pi_2\comp(F\pi_1)^\op\comp\sappr\\
+		=&\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr
+	\end{align*}
+	We prove that $\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr=\bar{F}r$. It is obvious that $\bar{F}r\subseteq(\appr\comp\bar{F}r)$, and $\bar{F}r\subseteq(\bar{F}r\comp\sappr)$. Assuming $x\mathrel{(\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr)} y$ then we have $x\mathrel{(\appr\comp\bar{F}r)} y$ and $x\mathrel{(\bar{F}r\comp\sappr)} y$, so by $x\mathrel{(\appr\comp\bar{F}r)} y$ there exists $y'$ such that $x\mathrel{\bar{F}r}y'$ and $y'\appr y$. In fact, $y'\appr y$ gives either of the following cases:
+	\begin{itemize}
+		\item $y=y'$: In this case we directly have $x\mathrel{\bar{F}r}y$.
+		\item $y'=\bot$: In this case we have $x\mathrel{\bar{F}r}\bot$ that means $x\mathrel{(\pi_2+1\comp(\pi_1+1)^\op)}\bot$ so there exists $z$ such that $\pi_2+1(z)=\bot$ that entails $z=\bot$ meaning that $x=\bot$. Recalling $x\mathrel{(\bar{F}r\comp\sappr)} y$, there exists $x'$ such that $x'\appr x$ and $x' \mathrel{\bar{F}r}y$. Since $x=\bot$ then $x'\appr x$ gives $x'=\bot$ that entails $x=x'$. So, from $x'\mathrel{\bar{F}r}y$ we have $x\mathrel{\bar{F}r}y$. 
+	\end{itemize}
+	So, we have $(\appr\comp\bar{F}r)\subseteq\bar{F}r$ that entails $(\appr\comp\bar{F}r\cap \bar{F}r\comp\sappr)\subseteq\bar{F}r$.\qed
+\end{proof}
+\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}
 \end{document}