From 0038476bbe049029a2b31f7651440438c53fb994 Mon Sep 17 00:00:00 2001 From: partowp Date: Wed, 26 Aug 2026 19:19:22 +0100 Subject: [PATCH] todo --- draft/draft.tex | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 6c8cd7a..4da85ab 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1178,7 +1178,7 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section %\end{definition} \begin{definition}[Relator-based Simulation] - Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if there is a morphism in $\rel$ from $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$, i.e, if $(x,y)\in R$ entails $(\alpha(x),\beta(y))\in\relar R$, for all $x\in X$ and $y\in Y$. + Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if there is a morphism in $\rel_a$ from $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$, i.e, if $(x,y)\in R$ entails $(\alpha(x),\beta(y))\in\relar R$, for all $x\in X$ and $y\in Y$. \end{definition} % \begin{definition}[Symmetric Relator] @@ -1196,8 +1196,22 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section \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$). \end{example} +% +\begin{prop}\label{prop:HeJ-HuJ} + Every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$: + \begin{itemize} + \item is a Hughes-Jacobs simulation if it is a Hermida-Jacobs simulation. + \item is a Hermida-Jacobs simulation if it is a Hermida-Jacobs simulation, assuming the axiom of choice. + \end{itemize} +\end{prop} +\begin{proof} + \todo{Finish!} +\end{proof} +\begin{rem} + The proposition entails that Hermida-Jacobs simulation subsumes Hughes-Jacobs simulation. +\end{rem} \subsection{Simulations in Double Categories} - +\todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!} %We show the category of partially ordered sets with monotone functions between them with $\poset$. %\begin{definition}[A Partial Order Over a Functor] % Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes: