Still revising the text!
This commit is contained in:
partowp
+60
-26
@@ -672,7 +672,7 @@ Now, we prove $Sg(\mu') = \nu$.
|
||||
%an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
|
||||
%We define the category of spans and relations.
|
||||
\begin{definition}[Category of Spans]\ppnote{Paul Levy said he doesn't like this name for this category as "category of spans" is used for a different category that is a bicategory.}
|
||||
For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, whenever the following diagram commutes:
|
||||
For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ (called \emph{witness}) in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, whenever the following diagram commutes:
|
||||
\begin{equation*}
|
||||
\begin{tikzcd}[ampersand replacement=\&]
|
||||
{X_1} \& R \& {X_2} \\
|
||||
@@ -692,13 +692,20 @@ Now, we prove $Sg(\mu') = \nu$.
|
||||
A pair of morphisms $p_1\c R\to X$ and $p_2\c R\to Y$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$.
|
||||
\end{definition}
|
||||
%
|
||||
\begin{prop}
|
||||
\begin{prop}\label{prop:joint-mon-unique}
|
||||
Given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$, assuming $q_1$ and $q_2$ are jointly monic, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then $w$ is unique.\qed
|
||||
\end{prop}
|
||||
%
|
||||
\begin{prop}\label{prop:joint-mon-pair}
|
||||
In a category $\BC$ with products, two morphisms $p_1\c R\to X$ and $p_2\c R \to Y$ are jointly monic iff $\brks{p_1,p_2}\c R\to X\times Y$ is monic.\qed
|
||||
\end{prop}
|
||||
%
|
||||
\begin{definition}[Category of Relations]
|
||||
For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
|
||||
For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is a full subcategory of $\spa(\BC)$ such that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel(\BC)$, $p_1$ and $p_2$ are jointly monic. %A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
|
||||
\end{definition}
|
||||
\begin{remark}
|
||||
Followed by~\autoref{prop:joint-mon-unique}, given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel(\BC)$, for morphisms $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$ in $\BC$, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then for every $v\c R\to S$, such that $(g_1,g_2,v)$ is a morphism in $\rel(\BC)$, then $v=w$.
|
||||
\end{remark}
|
||||
%
|
||||
%\begin{prop}
|
||||
% Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel(\BC)$ and $\spa(\BC)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel(\BC)$.
|
||||
@@ -709,32 +716,61 @@ For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary
|
||||
%
|
||||
\subsection{Spans and Relations in $\Set$}
|
||||
From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ accordingly. There are two choices for defining morphisms in each of the categories $\spa$ and $\rel$, namely \emph{anonymous} and \emph{onymous}. The already introduced type of morphisms is onymous. For functions $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2) \to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ is an anonymous morphism in $\spa$ if:
|
||||
\begin{gather*}
|
||||
\begin{gather}\label{eq:ano-morph}
|
||||
u\in R\Rightarrow \exists v\in S, q_1(v)= g_1\comp p_1(u) \quad\&\quad q_2(v)=g_2\comp p_2(u)
|
||||
\end{gather*}
|
||||
In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that forces the elements of relations to be pairs and the existential quantifier refers to a unique element:
|
||||
\begin{gather*}
|
||||
(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
|
||||
\end{gather*}
|
||||
\end{gather}
|
||||
% In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that forces the elements of relations to be pairs and the existential quantifier refers to a unique element:
|
||||
%\begin{gather*}
|
||||
% (x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
|
||||
%\end{gather*}
|
||||
From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to denote the categories of spans and relations with onymous morphisms.
|
||||
\begin{lemma}\label{lem:rel-iso}
|
||||
For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R^\dagger\subseteq X_1\times X_2$ and an bijection $r\c R\to R^\dagger$, such that
|
||||
\begin{gather*}
|
||||
\forall u\in R,\; p_1(u)=x_1\;\&\; p_2(u)=x_2\iff r(u)=(x_1,x_2).
|
||||
\end{gather*}
|
||||
\end{lemma}
|
||||
\begin{proof}
|
||||
By~\autoref{prop:joint-mon-pair} since $\Set$ has products $\brks{p_1,p_2}$ is monic. We take $R^\dagger$ as the image of $\brks{p_1,p_2}$ and we take $r\c R\to R^\dagger$ as the epimorphism in the image factorization of $\brks{p_1,p_2}$. Since $\brks{p_1,p_2}$ is monic, $r$ is a bijection. Now, the mentioned property is trivial.
|
||||
\end{proof}
|
||||
\begin{cor}\label{cor:rel-iso}
|
||||
For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R^\dagger\subseteq X_1\times X_2$ and an bijection $r\c R\to R^\dagger$, such that for every $(x_1,x_2)\in R^\dagger$,
|
||||
\begin{gather*}
|
||||
p_1\comp r^{-1}(x_1,x_2)=x_1\quad\&\quad p_2\comp r^{-1}(x_1,x_2)=x_2.
|
||||
\end{gather*}
|
||||
\end{cor}
|
||||
\begin{proof}
|
||||
The mentioned $r$ exists by~\autoref{lem:rel-iso}. For every $(x_1,x_2)\in R^\dagger$ there exists a unique $u\in R$ such that $r(u)=(x_1,x_2)$, and it means that $p_1(u)=x_1$ and $p_2(u)=x_2$, so we have $u=r^\mone(x_1,x_2)$ that means $p_1\comp r^\mone(x_1,x_2)=x_1$ and $p_2\comp r^\mone(x_1,x_2)=x_2$.\qed
|
||||
\end{proof}
|
||||
%
|
||||
\begin{prop}\label{prop:rel-rela}
|
||||
Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\rel_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness\sgnote{Unique?} $w\c R\to S$.
|
||||
Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\rel$ and $\rel_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the unique witness $w\c R\to S$.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
$(\Rightarrow):$ For every $(x_1,x_2)\in R$ we define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have:
|
||||
% $(\Rightarrow):$ We define $w$ as $w=\brks{g_1\comp p_1,g_2\comp p_2}$. We have:
|
||||
% \begin{align*}
|
||||
% g_1\comp p_1(x_1,x_2)&\\
|
||||
% =&g_1(x_1)\\
|
||||
% =&q_1(g_1(x_1),g_2(x_2))\\
|
||||
% =&q_1\comp w(x_1,x_2)
|
||||
% \end{align*}
|
||||
% Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
|
||||
$(\Rightarrow)$: By~\autoref{lem:rel-iso} there exist bijections $r\c R\to R^\dagger$ and $s\c S\to S^\dagger$ with the mentioned property. Since $(g_1,g_2)$ is a morphism from $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, for every $(x_1,x_2)\in R^\dagger$ we have $(g_1(x_1),g_2(x_2))\in S^\dagger$. So, we define $w'\c R^\dagger\to S^\dagger$ as $w'(x_1,x_2)=(g_1(x_1),g_2(x_2))$, and we define $w\c R\to S$ as $w=s^\mone\comp w'\comp r$. For every $u\in R$ and $i\in\{1,2\}$ we have:
|
||||
\begin{align*}
|
||||
g_1\comp p_1(x_1,x_2)&\\
|
||||
=&g_1(x_1)\\
|
||||
=&q_1(g_1(x_1),g_2(x_2))\\
|
||||
=&q_1\comp w(x_1,x_2)
|
||||
q_i\comp w(u)\\
|
||||
=&q_i\comp s^\mone\comp w'\comp r(u)\\
|
||||
=&q_i\comp s^\mone\comp w'(x_1,x_2)\\
|
||||
=&q_i\comp s^\mone(g_1(x_1),g_2(x_2))\\
|
||||
=&g_i(x_i)&\by{\autoref{cor:rel-iso}}\\
|
||||
=&g_i(p_i(u))\\
|
||||
=&g_i\comp p_i(u)
|
||||
\end{align*}
|
||||
Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
|
||||
|
||||
$(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed
|
||||
$(\Leftarrow):$ Assuming $u\in R$ we take $w(u)\in S$ as $v$ in~\eqref{eq:ano-morph}. We have $q_1(w(u))=p_1\comp g_1(u)$ and $q_2(w(u))=p_2\comp g_2(u)$ since $(g_1,g_2,w)$ is the morphism of the mentioned type.\qed
|
||||
\end{proof}
|
||||
|
||||
\begin{prop}\label{prop:spa-spaa}
|
||||
Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
|
||||
Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
($\Rightarrow$): We need the axiom of choice to prove this statement. By the definition of anonymous morphisms, for every $u\in R$ there exists $v\in S$ such that $q_1(v)=p_1\comp g_1(u)$ and $q_2(v)=p_2\comp g_2(u)$. So, for each $u\in R$ there exists a set $V_u\in\powf S$ that its elements have the mentioned properties. We can form a function $h\c R\to \powf S$ that $h(u)=V_u$. The image of $h$ that we denote with $\im(h)$ is a family of non-empty sets. By the axiom of choice, there exists a function $s\c \im(h)\to S$. We define $w\c R\to S$ as $w=s\comp h$, then for every $u\in R$, we have $q_1\comp w(u)=g_1\comp p_1(u)$ and $q_2\comp w(u)=g_2\comp p_2(u)$.
|
||||
@@ -742,13 +778,11 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
|
||||
($\Leftarrow$): Assuming $u\in R$, there exists $w(u)\in S$, and by the definition of onymous morphisms we have $q_1(w(u))=g_1\comp p_1(u)$ and $q_2(w(u))=g_2\comp p_2(u)$. \qed
|
||||
\end{proof}
|
||||
|
||||
\begin{prop}\label{prop:rela-spaa}\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
|
||||
Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
|
||||
\begin{prop}\label{prop:rela-spaa}%\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
|
||||
Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
($\Rightarrow$): Assuming that $(g_1,g_2)$ is a morphism in $\spa_a$, then for $(x_1,x_2)\in R$ there exists $v\in S$, such that $q_1(v)=g_1(x_1)$ and $q_2(v)=g_2(x_2)$. Since $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)\in\rel_a$ then the $v$ is unique and $v=(g_1(x_1),g_2(x_2))$.
|
||||
|
||||
($\Leftarrow$): As $\rel_a$ is a subcategory of $\spa_a$, this is trivial.\qed
|
||||
It is trivial as $\rel_a$ is a full subcategory of $\spa_a$\qed
|
||||
\end{proof}
|
||||
|
||||
\begin{prop}\label{prop:rel-spa}
|
||||
@@ -1347,7 +1381,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
|
||||
\begin{enumerate}
|
||||
\item Assuming the axiom of choice span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an Aczel-Mendler bisimulation iff it is a span-based bisimulation.
|
||||
\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is a Hughes-Jacobs bisimulation.
|
||||
\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.
|
||||
\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
|
||||
\end{enumerate}
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
@@ -1542,8 +1576,8 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
|
||||
\begin{prop}\label{prop:HeJ-HuJ}
|
||||
Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$,
|
||||
\begin{enumerate}
|
||||
\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.
|
||||
\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a $\tilde{F}$-simulation, assuming the axiom of choice.
|
||||
\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
|
||||
\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a $\tilde{F}$-simulation, assuming the axiom of choice.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
|
||||
\end{enumerate}
|
||||
\end{prop}
|
||||
\begin{proof}
|
||||
|
||||
Reference in New Issue
Block a user