diff --git a/draft/draft.tex b/draft/draft.tex index 003d259..271cbad 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -293,6 +293,7 @@ \newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,0.07);}}} \newcommand{\powf}{\mathcal{P}} \newcommand{\sappr}{\sqsupseteq} +\newcommand{\Dom}{\mathsf{Dom}} \newcommand{\simeet}{% \mathbin{% @@ -2192,18 +2193,18 @@ Now, we prove our main statement. \end{cor} Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor. \subsection{Maybe Functor} -We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_{X+1}\cup\{(\bot,x)\mid x\in X\}$.\\ +We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for sets $X$ and $Y$, and functions $f,g\c X\to Y+1$ we have $f\appr g$ whenever $\Dom(f)\subseteq\Dom(g)$ ($\Dom(f)$ is the domain of a function $f$). Now, we prove that the given order on the maybe functor is a liftable one. \begin{lemma}\label{lem:maybe-lif} 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 $h\appr Fg(k)$, 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 $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$. - - \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} +% 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 $h\appr Fg(k)$, 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 $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$. +% \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} +Assuming that $h\in\Hom(X,Z+1)$, $g\c Y\to Z$, $k\in\Hom(X,Y+1)$, such that $h\appr (g+1)\comp k$ \end{proof} \begin{lemma}\label{lem:maybe-colif} The order structure on the set-functor $FX=X+1$ is a coliftable order. @@ -2293,28 +2294,28 @@ So, proven by Dubut, for every AM-simulation relation over a coalgebra $(X,\alph \begin{proof} We prove that $\sigma$ also is a witness for $R$ to be an AM-bisimulation. For every $(x_1,x_2)\in R$ we have \begin{enumerate} - \item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}, - \item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\ + \item $\alpha(x_1)=(p_1+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}, + \item $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4},\\ % \end{enumerate} and since $R$ is symmetric, we have % \begin{enumerate} - \item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}, - \item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}, + \item $\alpha(x_2)=(p_1+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}, + \item $\alpha(x_1)\sappr (p_2+1)\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}, \end{enumerate} - Followed by $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$ we have the following cases: + Followed by $\alpha(x_2)\sappr (p_2+1)\comp\sigma(x_1,x_2)$ we have the following cases: \begin{itemize} - \item $\alpha(x_2)=p_2+1\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation. - \item $Fp_2\comp\sigma(x_1,x_2)=\bot$: In this case, we have + \item $\alpha(x_2)=(p_2+1)\comp\sigma(x_1,x_2)$: In this case, we already have $\sigma$ as a witness for $R$ to be a bisimulation. + \item $p_2+1\comp\sigma(x_1,x_2)=\bot$: In this case, we have \begin{align*} - p_2+1\comp\sigma(x_1,x_2)=\bot,&\\ + (p_2+1)\comp\sigma(x_1,x_2)=\bot,&\\ \Rightarrow&\sigma(x_1,x_2)=\bot,\\ - \Rightarrow&p_1+1\comp\sigma(x_1,x_2)=\bot,\\ + \Rightarrow&(p_1+1)\comp\sigma(x_1,x_2)=\bot,\\ \Rightarrow&\alpha(x_1)=\bot,&\eqref{eq:maybe-func-set-1}\\ - \Rightarrow&p_2+1\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\ + \Rightarrow&(p_2+1)\comp\sigma(x_2,x_1)=\bot,&\eqref{eq:maybe-func-set-3}\\ \Rightarrow&\sigma(x_2,x_1)=\bot,\\ - \Rightarrow&p_1+1\comp\sigma(x_2,x_1)=\bot,\\ + \Rightarrow&(p_1+1)\comp\sigma(x_2,x_1)=\bot,\\ \Rightarrow&\alpha(x_2)=\bot,&\eqref{eq:maybe-func-set-2}\\ - \Rightarrow&\alpha(x_2)=p_1+1\comp\sigma(x_1,x_2). + \Rightarrow&\alpha(x_2)=(p_1+1)\comp\sigma(x_1,x_2). \end{align*} \end{itemize}\qed \end{proof} @@ -3101,7 +3102,7 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \begin{proof} \todo{Finish.} \end{proof} -\subsection{Symmetrization of a Barr relator} +\subsection{Symmetrization of a lax Barr relator} \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}