From 4471bf385b66fad58e84346cab25324e8c9b9c15 Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 14 Jul 2026 18:24:23 +0100 Subject: [PATCH] prop --- draft/draft.tex | 38 +++++++++++++++++++++++++++++++++++--- 1 file changed, 35 insertions(+), 3 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 123f937..03d1f1f 100644 --- a/draft/draft.tex +++ b/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} - The mentioned order on the maybe functor is not coliftable. -\end{remark} +\begin{lemma}\label{lem:maybe-colif} + The order structure on the set-functor $FX=X+1$ is a liftable order. +\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}