pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

edited

Browse Source
This commit is contained in:
partowp 2026-04-19 00:10:59 +01:00
parent a888ed095a
commit e8a4210c0e
1 changed files with 13 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
draft/draft.tex
View File

@ -1849,15 +1849,17 @@ Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\d
\arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3]
\end{tikzcd}
\end{equation*}
$\delta$ is defined as the following:
To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger$ and $u\c((\mathcal{P}R^\dagger)\times R)+(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$:
\begin{gather*}
\delta(w)=
c(w)=
\begin{cases}
(\alpha(x_1),\alpha(x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w \\
w & \mathsf{o.w}
\end{cases}
\inl(w,(x_1,x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w \\
\inr w & \mathsf{o.w}
\end{cases}\\
u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
u(\inr w)=w
\end{gather*}
Now, we want to prove an abstraction of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram:
Now, we want to prove a more abstract version of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram:
\begin{equation*}
\begin{tikzcd}[ampersand replacement=\&]
{\appr;(FR)^\dagger;\appr} \& {\appr;(FR)^\dagger} \& {\appr} \& {FX} \\
@ -1870,15 +1872,15 @@ Now, we want to prove an abstraction of this statement. First, we need to spell
\arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3]
\arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
\arrow["{{{{{{{i_1}}}}}}}", from=1-3, to=1-4]
\arrow["{{{{{{{i_2}}}}}}}", from=1-3, to=2-3]
\arrow["{{{{{{{q_1}}}}}}}", from=1-3, to=1-4]
\arrow["{{{{{{{q_2}}}}}}}", from=1-3, to=2-3]
\arrow["{{{{{{{Fp_1^\dagger}}}}}}}", from=2-2, to=2-3]
\arrow["{{{{{{{Fp_2^\dagger}}}}}}}"', from=2-2, to=3-2]
\arrow["{{{{{{{i_1}}}}}}}"', from=3-1, to=3-2]
\arrow["{{{{{{{i_2}}}}}}}"', from=3-1, to=4-1]
\arrow["{{{{{{{q_1}}}}}}}"', from=3-1, to=3-2]
\arrow["{{{{{{{q_2}}}}}}}"', from=3-1, to=4-1]
\end{tikzcd}
\end{equation*}
Additionally, we make the abbreviations that ${Fp_1}_\appr=i_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=i_2\comp\pi_2$.
Additionally, we make the abbreviations that ${Fp_1}_\appr=q_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=q_2\comp\pi_2$.
\begin{prop}
Assuming we have a morphism $\sigma'\c R\to(FR)^\dagger$ then exists $\delta\c(FR)^\dagger\to(\appr;(FR)^\dagger;\appr)^\dagger$ such that $\sigma=\delta\comp\sigma'$ that commutes in the following diagram:
\begin{equation*}