From dde56ad7d8fdb2799f7317d24628a2a7a7483a15 Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 11 Sep 2026 13:55:06 +0100 Subject: [PATCH] minor --- draft/draft.tex | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index c09517c..7c8f56c 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1454,19 +1454,19 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section \end{example} % \begin{example} - Given $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{q_2}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote this relator with $F^\leftrightarrow$. + Given $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{q_2}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote this relator with $\tilde{F}$. \end{example} % \begin{prop}\label{prop:HeJ-HuJ} - For a functor $F\c\Set\to\Set$, every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ from a coalgebra $(X,\alpha)$ to $(Y,\beta)$: + For a functor $F\c\Set\to\Set$, every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$: \begin{enumerate} - \item is a $F^\leftrightarrow$-simulation if it is a Hermida-Jacobs simulation. - \item is a Hermida-Jacobs simulation if it is a $F^\leftrightarrow$-simulation, assuming the axiom of choice. + \item is a $\tilde{F}$-simulation if it is a Hermida-Jacobs simulation. + \item is a Hermida-Jacobs simulation if it is a $\tilde{F}$-simulation, assuming the axiom of choice. \end{enumerate} \end{prop} \begin{proof} - (1): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a Hermida-Jacobs simulation means that for every $(x,y)\in R$, we have $\alpha\comp p_1(x,y)\appr(Fp_1)^\dagger\comp\sigma(x,y)$ and $(Fp_2)^\dagger\comp\sigma(x,y)\appr\beta\comp p_2(x,y)$. So, $x\mathrel{R}y$ gives that $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means that $R$ is a $F^\leftrightarrow$-simulation.\\ - (2): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a $F^\leftrightarrow$-simulation means that $x\mathrel{R}y$ gives $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means for every $(x,y)\in R$, there exist $(u,v)\in(FR)^\dagger$ such that $\alpha(x)\appr u$ and $v\appr\beta(y)$. We form a function $f\c R\to\powf(FR)^\dagger$ such that takes every $(x,y)$ to the set of the mentioned existing pairs $(u,v)$ in $(FR)^\dagger$. By the axiom of choice there exist a function $s\c\im_f\to(FR)^\dagger$. So, assuming that $f$ has the epi-mono factorization $(e,m)$, then we define $\sigma\c R\to(FR)^\dagger$ as $\sigma=s\comp e$. Now, the diagram~\eqref{eq:diag-hj-sim} commutes laxly for the defined $\sigma$.\qed + (1): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a Hermida-Jacobs simulation means that for every $(x,y)\in R$, we have $\alpha\comp p_1(x,y)\appr(Fp_1)^\dagger\comp\sigma(x,y)$ and $(Fp_2)^\dagger\comp\sigma(x,y)\appr\beta\comp p_2(x,y)$. So, $x\mathrel{R}y$ gives that $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means that $R$ is a $\tilde{F}$-simulation.\\ + (2): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a $\tilde{F}$-simulation means that $x\mathrel{R}y$ gives $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means for every $(x,y)\in R$, there exist $(u,v)\in(FR)^\dagger$ such that $\alpha(x)\appr u$ and $v\appr\beta(y)$. We form a function $f\c R\to\powf(FR)^\dagger$ such that takes every $(x,y)$ to the set of the mentioned existing pairs $(u,v)$ in $(FR)^\dagger$. By the axiom of choice there exist a function $s\c\im_f\to(FR)^\dagger$. So, assuming that $f$ has the epi-mono factorization $(e,m)$, then we define $\sigma\c R\to(FR)^\dagger$ as $\sigma=s\comp e$. Now, the diagram~\eqref{eq:diag-hj-sim} commutes laxly for the defined $\sigma$.\qed \end{proof} \begin{rem} The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.