$\mathsf{T}\operatorname{th}_{\mathfrak{X}}(\gamma(x))\in\lambda_{\mathbb{Z}}(\widetilde{\varphi}_{1},\ldots,\widetilde{\varphi}_{n})\quad\text{iff}\quad\zeta(\operatorname{th}_{\mathfrak{X}}(x))\in\lambda_{\mathbb{Z}}(\widetilde{\varphi}_{1},\ldots,\widetilde{\varphi}_{n}).$

This follows from the following computation,

$\displaystyle\mathsf{T}\operatorname{th}_{\mathfrak{X}}(\gamma(x))$
$\displaystyle\in\lambda_{\mathbb{Z}}(\widetilde{\varphi}_{1},\ldots,\widetilde{\varphi}_{n})$
$\displaystyle\text{iff}\quad\gamma(x)\in(\mathsf{T}\operatorname{th}_{\mathfrak{X}})^{-1}(\lambda_{\mathbb{Z}}(\widetilde{\varphi}_{1},\ldots,\widetilde{\varphi}_{n}))$
$\displaystyle\text{iff}\quad\gamma(x)\in\lambda_{\mathbb{X}}(\operatorname{th}_{\mathfrak{X}}^{-1}(\widetilde{\varphi}_{1}),\ldots,\operatorname{th}_{\mathfrak{X}}^{-1}(\widetilde{\varphi}_{n}))$
(Naturality of $\lambda$)
$\displaystyle\text{iff}\quad\gamma(x)\in\lambda_{\mathbb{X}}(\llbracket\varphi_{1}\rrbracket^{\mathfrak{X}},\ldots,\llbracket\varphi_{n}\rrbracket^{\mathfrak{X}})$
(By (12))
$\displaystyle\text{iff}\quad\mathfrak{X},x\Vdash\heartsuit^{\lambda}(\varphi_{1},\ldots,\varphi_{n})$
(Definition of $\Vdash$)
$\displaystyle\text{iff}\quad\heartsuit^{\lambda}(\varphi_{1},\ldots,\varphi_{n})\in\operatorname{th}_{\mathfrak{X}}(x)$
(Definition of $\operatorname{th}_{\mathfrak{X}}$)
$\displaystyle\text{iff}\quad\zeta(\operatorname{th}_{\mathfrak{X}}(x))\in\lambda_{\mathbb{Z}}(\widetilde{\varphi}_{1},\ldots,\widetilde{\varphi}_{n})$
(Definition of $\zeta$)

This proves the proposition.

The developed theory results in the following theorem.

######  Theorem 39.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{Top}$ which preserves sobriety,
and $\Lambda$ a Scott-continuous characteristic geometric modal signature for
$\mathsf{T}$. Then the geometric $\mathsf{T}$-model
$\mathfrak{Z}=(\mathbb{Z},\zeta,V_{\mathbb{Z}})$ is final in
$\mathbf{Mod}(\mathsf{T})$.

######  Proof 7.6.

Proposition 38 states that for every geometric $\mathsf{T}$-model
$\mathfrak{X}=(\mathbb{X},\gamma,V)$ there exists a $\mathsf{T}$-coalgebra
morphism $\operatorname{th}_{\mathfrak{X}}:\mathfrak{X}\to\mathfrak{Z}$, so we
only need to show that this morphism is unique.

Let $f:\mathfrak{X}\to\mathfrak{Z}$ be any coalgebra morphism. We know from
Proposition 9 that coalgebra morphisms preserve truth, so for all
$x\in\mathbb{X}$ we have $\varphi\in f(x)$ iff
$\mathfrak{Z},f(x)\Vdash\varphi$ iff $\mathfrak{X},x\Vdash\varphi$. Therefore
we must have $f(x)=\operatorname{th}_{\mathfrak{X}}(x)$.

As an immediate corollary we obtain the following theorem. Recall from
Definition 3.2 that two states $x$ and $x^{\prime}$ are behaviourally
equivalent in $\mathbf{Mod}(\mathsf{T})$ if there are $\mathsf{T}$-model
morphisms $f$ and $f^{\prime}$ with $f(x)=f^{\prime}(x^{\prime})$.

######  Theorem 40.

Under the assumptions of Theorem 39, we have
${\equiv_{\Lambda}}=\,{\simeq_{\mathbf{Mod}(\mathsf{T})}}$.

######  Proof 7.7.

If $x$ and $x^{\prime}$ are behaviourally equivalent, then they are modally
equivalent by Proposition 9. Conversely, if they are modally equivalent, then
$\operatorname{th}_{\mathfrak{X}}(x)=\operatorname{th}_{\mathfrak{X}^{\prime}}(x^{\prime})$
by construction, so they are behaviourally equivalent.

######  Remark 41.

If $\mathsf{T}$ is an endofunctor on $\mathbf{Sob}$ instead of $\mathbf{Top}$,
then the same procedure yields a final model in $\mathbf{Mod}(\mathsf{T})$. In
particular, $\mathsf{T}$ need not be the restriction of a
$\mathbf{Top}$-endofunctor. However, if $\mathsf{T}$ is an endofunctor on
$\mathbf{KSob}$ or $\mathbf{KHaus}$ the procedure above does not guarantee a
final coalgebra in $\mathbf{Mod}(\mathsf{T})$; indeed the state space
$\mathbb{Z}$ of the final coalgebra $\mathfrak{Z}$ we just constructed need
not be compact sober nor compact Hausdorff.

Of course, there may be a different way to attain similar results for
$\mathbf{KSob}$ or $\mathbf{KHaus}$. We leave this as an interesting open
question. In Theorem 48 we prove an analog of Theorem 40 for endofunctors on
$\mathbf{KSob}$.

##  8\. Bisimulations

This section is devoted to bisimulations and bisimilarity between coalgebraic
geometric models. We compare two notions of bisimilarity, modal equivalence
(from Definition 3.2) and behavioural equivalence (Definition 3.2). Again,
where $\mathbf{C}$ is be a full subcategory of $\mathbf{Top}$ and $\mathsf{T}$
an endofunctor on $\mathbf{C}$, we give definitions and propositions in this
generality where possible. When necessary, we will restrict our scope to
particular instances of $\mathbf{C}$.

Let $\mathfrak{X}=(\mathbb{X},\gamma,V)$ and
$\mathfrak{X}^{\prime}=(\mathbb{X}^{\prime},\gamma^{\prime},V^{\prime})$ be
two geometric $\mathsf{T}$-models. Let $\mathbb{B}$ be an object in
$\mathbf{C}$ such that
$\mathbb{B}\subseteq\mathbb{X}\times\mathbb{X}^{\prime}$, with projections
$\pi:\mathbb{B}\to\mathbb{X}$ and
$\pi^{\prime}:\mathbb{B}\to\mathbb{X}^{\prime}$. Then $\mathbb{B}$ is called
an _Aczel-Mendler bisimulation_ between $\mathfrak{X}$ and
$\mathfrak{X}^{\prime}$ if for all $(x,x^{\prime})\in\mathbb{B}$ we have $x\in
V(p)$ iff $x^{\prime}\in V^{\prime}(p)$ and there exists a transition map
$\beta:\mathbb{B}\to\mathsf{T}\mathbb{B}$ that makes $\pi$ and $\pi^{\prime}$
coalgebra morphisms. That is, $\beta$ is such that the following diagram
commutes:

${\mathbb{X}}$${\mathbb{B}}$${\mathbb{X}^{\prime}}$${\mathsf{T}\mathbb{X}}$${\mathsf{T}\mathbb{B}}$${\mathsf{T}\mathbb{X}^{\prime}}$$\scriptstyle{\gamma}$$\scriptstyle{\pi}$$\scriptstyle{\pi^{\prime}}$$\scriptstyle{\beta}$$\scriptstyle{\gamma^{\prime}}$$\scriptstyle{\mathsf{T}\pi}$$\scriptstyle{\mathsf{T}\pi^{\prime}}$

Two states
$x\in\mathsf{U}\mathbb{X},x^{\prime}\in\mathsf{U}\mathbb{X}^{\prime}$ are
called _bisimilar_ , notation $x\leftrightarroweq x^{\prime}$, if they are
linked by a coalgebra bisimulation.

It follows from Proposition 9 that bisimilar states satisfy the same formulas.
Furthermore, it easily follows by taking pushouts that Aczel-Mendler
bisimilarity implies behavioural equivalence. If moreover $\mathsf{T}$
preserves weak pullbacks, the converse holds as well [34].

However, we do not wish to make this assumption on topological spaces, since
few functors seem to preserve weak pullbacks. For example, the Vietoris
functor does not preserve weak pullbacks [7, Corollary 4.3] and neither does
the monotone functor from Definition 4.2. (To see the latter statement,
consider the example given in Section 4 of [18] and equip the sets in use with
the discrete topology.) Therefore we define $\Lambda$-bisimulations for
$\mathbf{Top}$-coalgebras as an alternative to Aczel-Mendler bisimulations.
This notion is an adaptation of ideas in [3, 15]. Under some conditions on
$\Lambda$, $\Lambda$-bisimilarity coincides with behavioural equivalence.

In the next definition we need the concept of coherent pairs: If $X$ and
$X^{\prime}$ are two sets and $B\subseteq X\times X^{\prime}$ is a relation,
then a pair $(a,a^{\prime})\in\mathsf{P}X\times\mathsf{P}X^{\prime}$ is called
_$B$ -coherent_ if $B[a]\subseteq a^{\prime}$ and $B^{-1}[a^{\prime}]\subseteq
a$. For details and properties see Section 2 in [19].

Let $\mathsf{T}$ be an endofunctor on $\mathbf{C}$, $\Lambda$ a geometric
modal signature for $\mathsf{T}$ and $\mathfrak{X}=(\mathbb{X},\gamma,V)$ and
$\mathfrak{X}^{\prime}=(\mathbb{X}^{\prime},\gamma^{\prime},V^{\prime})$ two
geometric $\mathsf{T}$-models. A _$\Lambda$ -bisimulation_ between
$\mathfrak{X}$ and $\mathfrak{X}^{\prime}$ is a relation
$B\subseteq\mathsf{U}\mathbb{X}\times\mathsf{U}\mathbb{X}^{\prime}$ such that
for all $(x,x^{\prime})\in B$ and $p\in\Phi$ and all tuples of $B$-coherent
pairs of opens
$(a_{i},a_{i}^{\prime})\in\mathsf{\Omega}\mathbb{X}\times\mathsf{\Omega}\mathbb{X}^{\prime}$
we have

$x\in V(p)\quad\text{ iff }\quad x^{\prime}\in V^{\prime}(p)$

and

$\gamma(x)\in\lambda_{\mathbb{X}}(a_{1},\ldots,a_{n})\quad\text{iff}\quad\gamma^{\prime}(x^{\prime})\in\lambda_{\mathbb{X}^{\prime}}(a_{1}^{\prime},\ldots,a_{n}^{\prime}).$
(13)

Two states are called $\Lambda$-bisimilar if there is a $\Lambda$-bisimulation
linking them, notation: $x\leftrightarroweq_{\Lambda}x^{\prime}$.

We give an alternative characterisation of (13) to elucidate the connection
with [3].

######  Remark 42.

Let $B\subseteq\mathbb{X}\times\mathbb{X}^{\prime}$ be a relation endowed with
the subspace topology and let $\pi:B\to\mathbb{X}$ and
$\pi^{\prime}:B\to\mathbb{X}^{\prime}$ be projections. Then
$(a,a^{\prime})\in\mathsf{\Omega}\mathbb{X}\times\mathsf{\Omega}\mathbb{X}^{\prime}$
is $B$-coherent iff $\pi^{-1}(a)=(\pi^{\prime})^{-1}(a^{\prime})$.

Let $P$ be the pullback of the cospan
${\mathsf{\Omega}\mathbb{X}}$${\mathsf{\Omega}B}$${\mathsf{\Omega}\mathbb{X}^{\prime}}$$\scriptstyle{\mathsf{\Omega}\pi}$$\scriptstyle{\mathsf{\Omega}\pi^{\prime}}$
in $\mathbf{Frm}$ and let $p:P\to\mathbb{X}$ and
$p^{\prime}:P\to\mathbb{X}^{\prime}$ be the corresponding projections. Then
the $B$-coherent pairs are precisely $(p(x),p^{\prime}(x))$, where $x$ ranges
over $P$. It follows from the definitions that equation (13) holds for all
$B$-coherent pairs if and only if

$\mathsf{\Omega}\pi\circ\mathsf{\Omega}\gamma\circ\lambda_{\mathbb{X}}\circ
p^{n}=\mathsf{\Omega}\pi^{\prime}\circ\mathsf{\Omega}\gamma^{\prime}\circ\lambda_{\mathbb{X}^{\prime}}\circ(p^{\prime})^{n},$

where $\lambda$ is $n$-ary.

As desired, $\Lambda$-bisimilar states satisfy the same formulas.

######  Proposition 43.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{C}$ and $\Lambda$ a geometric
modal signature for $\mathsf{T}$. Then
${\leftrightarroweq_{\Lambda}}\subseteq{\equiv_{\Lambda}}$.

######  Proof 8.1.

Let $B$ be a $\Lambda$-bisimulation between geometric $\mathsf{T}$-models
$\mathfrak{X}$ and $\mathfrak{X}^{\prime}$, and suppose $xBx^{\prime}$. Using
induction on the complexity of the formula, we show that
$\mathfrak{X},x\Vdash\varphi$ iff
$\mathfrak{X}^{\prime},x^{\prime}\Vdash\varphi$ for all
$\varphi\in\operatorname{GML}(\Phi,\Lambda)$. The propositional case is by
definition, and $\wedge$ and $\bigvee$ are routine. Suppose
$\mathfrak{X},x\Vdash\heartsuit^{\lambda}(\varphi_{1},\ldots,\varphi_{n})$,
then
$\gamma(x)\in\lambda_{\mathbb{X}}(\llbracket\varphi_{1}\rrbracket^{\mathfrak{X}},\ldots,\llbracket\varphi_{n}\rrbracket^{\mathfrak{X}})$.
By the induction hypothesis
$(\llbracket\varphi_{i}\rrbracket^{\mathfrak{X}},\llbracket\varphi_{i}\rrbracket^{\mathfrak{X}^{\prime}})$
is $B$-coherent for all $i$. Then
$\gamma^{\prime}(x^{\prime})\in\lambda_{\mathbb{X}^{\prime}}(\llbracket\varphi_{1}\rrbracket^{\mathfrak{X}^{\prime}},\ldots,\llbracket\varphi_{n}\rrbracket^{\mathfrak{X}^{\prime}})$
since $B$ is a $\Lambda$-bisimulation, hence
$\mathfrak{X}^{\prime},x^{\prime}\Vdash\heartsuit^{\lambda}(\varphi_{1},\ldots,\varphi_{n})$.
The converse is proven symmetrically.

######  Proposition 44.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{C}$ and $\Lambda$ a geometric
modal signature for $\mathsf{T}$. Then
${\leftrightarroweq}\subseteq{\leftrightarroweq_{\Lambda}}$.

######  Proof 8.2.

It suffices to show that every Aczel-Mendler bisimulation is a
$\Lambda$-bisimulation. Suppose $B$ is an Aczel-Mendler bisimulation and let
$\beta$ be the map that turns $B$ into a coalgebra, then the following diagram
commutes:

${\mathbb{X}}$${B}$${\mathbb{X}^{\prime}}$${\mathsf{T}\mathbb{X}}$${\mathsf{T}B}$${\mathsf{T}\mathbb{X}^{\prime}}$$\scriptstyle{\gamma}$$\scriptstyle{\pi}$$\scriptstyle{\pi^{\prime}}$$\scriptstyle{\beta}$$\scriptstyle{\gamma^{\prime}}$$\scriptstyle{\mathsf{T}\pi}$$\scriptstyle{\mathsf{T}\pi^{\prime}}$
(14)

We will show that $B$ is a $\Lambda$-bisimulation. By definition $x\in V(p)$
iff $x^{\prime}\in V^{\prime}(p)$ whenever $xBx^{\prime}$. We prove the forth
condition from Definition 8. Let $\lambda\in\Lambda$ and $(x,x^{\prime})\in
B$. Suppose $(a_{1},a_{1}^{\prime}),\ldots,(a_{n},a_{n}^{\prime})$ are
$B$-coherent pairs of opens and
$\gamma(x)\in\lambda_{\mathbb{X}}(a_{1},\ldots,a_{n})$. Then we have

$\displaystyle\beta(x,x^{\prime})$
$\displaystyle\in(\mathsf{T}\pi)^{-1}(\lambda_{\mathbb{X}}(a_{1},\ldots,a_{n}))$
(Follows from (14))
$\displaystyle=\lambda_{B}(\pi^{-1}(a_{1}),\ldots,\pi^{-1}(a_{n}))$
(Naturality of $\lambda$)
$\displaystyle\subseteq\lambda_{B}\big{(}(\pi^{\prime})^{-1}\circ\pi^{\prime}[\pi^{-1}(a_{1})],\ldots,(\pi^{\prime})^{-1}\circ\pi^{\prime}[\pi^{-1}(a_{n})]\big{)}$
(Monotonicity of $\lambda$)
$\displaystyle=\lambda_{B}\big{(}(\pi^{\prime})^{-1}(B[a_{1}]),\ldots,(\pi^{\prime})^{-1}(B[a_{n}])\big{)}$
($B[a]=\pi^{\prime}\circ\pi^{-1}(a)$)
$\displaystyle\subseteq\lambda_{B}((\pi^{\prime})^{-1}(a_{1}^{\prime}),\ldots,(\pi^{\prime})^{-1}(a_{n}^{\prime}))$
(Monotonicity of $\lambda$)
$\displaystyle=(\mathsf{T}\pi^{\prime})^{-1}(\lambda_{\mathbb{X}^{\prime}}(a_{1}^{\prime},\ldots,a_{n}^{\prime})).$
(Naturality of $\lambda$)

Therefore

$\gamma^{\prime}(x^{\prime})=(\mathsf{T}\pi^{\prime})(\beta(x,x^{\prime}))\in\lambda_{\mathbb{X}^{\prime}}(a_{1}^{\prime},\ldots,a_{n}^{\prime}),$

as desired.

The collection of $\Lambda$-bisimulations between two models enjoys the
following interesting property.

######  Proposition 45.

Let $\Lambda$ be a geometric modal signature of a functor
$\mathsf{T}:\mathbf{Top}\to\mathbf{Top}$ and let
$\mathfrak{X}=(\mathbb{X},\gamma,V)$ and
$\mathfrak{X}^{\prime}=(\mathbb{X}^{\prime},\gamma^{\prime},V^{\prime})$ be
two geometric $\mathsf{T}$-models. The collection of $\Lambda$-bisimulations
between $\mathfrak{X}$ and $\mathfrak{X}^{\prime}$ forms a complete lattice.

######  Proof 8.3.

It is obvious that the collection of $\Lambda$-bisimulations is a poset. We
will show that this collection is closed under taking arbitrary unions; the
result then follows from the fact that any complete semilattice is also a
complete lattice, see e.g. [8, Theorem 4.2].

Let $J$ be some index set and for all $j\in J$ let $B_{j}$ be
$\Lambda$-bisimulations between $\mathfrak{X}$ and $\mathfrak{X}^{\prime}$ and
set $B=\bigcup_{j\in J}B_{j}$. We claim that $B$ is a $\Lambda$-bisimulation.

Let $(a_{i},a_{i}^{\prime})$ be $B$-coherent pairs of opens. Suppose
$xBx^{\prime}$ and $\gamma(x)\in\lambda_{\mathbb{X}}(a_{1},\ldots,a_{n})$.
Then there is $j\in J$ with $xB_{j}x^{\prime}$ hence $x\in V(p)$ iff
$x^{\prime}\in V^{\prime}(p)$. As $B_{j}[a_{i}]\subseteq B[a]\subseteq
a_{i}^{\prime}$ and $B_{j}^{-1}[a^{\prime}]\subseteq
B^{-1}[a^{\prime}]\subseteq a_{i}$, all $B$-coherent pairs
$(a_{i},a_{i}^{\prime})$ are also $B_{j}$-coherent. Since $B_{j}$ is a
$\Lambda$-bisimulation we get
$\gamma^{\prime}(x^{\prime})\in\lambda_{\mathbb{X}^{\prime}}(a_{1}^{\prime},\ldots,a_{n}^{\prime})$.
The converse direction is proven symmetrically.

We know by now that $\Lambda$-bisimilarity implies modal equivalence.
Furthermore, we have seen in Theorem 40 that modal equivalence coincides with
behavioural equivalence whenever $\mathsf{T}$ is an endofunctor on
$\mathbf{Top}$ which preserves sobriety and $\Lambda$ is a Scott-continuous
characteristic geometric modal signature. In order to prove a converse, i.e.
that behavioural equivalence implies $\Lambda$-bisimilarity, we need to assume
that the geometric modal signature is strong.

Recall that two elements $x,x^{\prime}$ in two models are behaviourally
equivalent in $\mathbf{Mod}(\mathsf{T})$, notation:
$\simeq_{\mathbf{Mod}(\mathsf{T})}$, if there exist morphisms $f,f^{\prime}$
in $\mathbf{Mod}(\mathsf{T})$ such that $f(x)=f^{\prime}(x^{\prime})$.

######  Proposition 46.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{C}$ and $\Lambda$ a strongly
monotone geometric modal signature for $\mathsf{T}$. Let
$\mathfrak{X}=(\mathbb{X},\gamma,V)$ and
$\mathfrak{X}^{\prime}=(\mathbb{X}^{\prime},\gamma^{\prime},V^{\prime})$ be
two geometric $\mathsf{T}$-models. Then
${\simeq_{\mathbf{Mod}(\mathsf{T})}}\subseteq{\leftrightarroweq_{\Lambda}}$.

######  Proof 8.4.

Suppose $x$ and $x^{\prime}$ are behaviourally equivalent. Then there are some
geometric $\mathsf{T}$-model $\mathfrak{Y}=(\mathbb{Y},\nu,V_{\mathbb{Y}})$
and $\mathsf{T}$-model morphisms $f:\mathfrak{X}\to\mathfrak{Y}$ and
$f^{\prime}:\mathfrak{X}^{\prime}\to\mathfrak{Y}$ such that
$f(x)=f^{\prime}(x^{\prime})$. We will show that

$B=\\{(u,u^{\prime})\in X\times X^{\prime}\mid
f(u)=f^{\prime}(u^{\prime})\\}.$ (15)

is a $\Lambda$-bisimulation $B$ linking $x$ and $x^{\prime}$.

Clearly $xBx^{\prime}$. It follows from Proposition 9 that $u$ and
$u^{\prime}$ satisfy precisely the same formulas whenever $(u,u^{\prime})\in
B$. Suppose $\lambda\in\Lambda$ is $n$-ary and for $1\leq i\leq n$ let
$(a_{i},a_{i}^{\prime})$ be a $B$-coherent pair of opens. Suppose
$uBu^{\prime}$ and $\gamma(u)\in\lambda_{\mathbb{X}}(a_{1},\ldots,a_{n})$. We
will show that
$\gamma^{\prime}(u^{\prime})\in\lambda_{\mathbb{X}^{\prime}}(a_{1}^{\prime},\ldots,a_{n}^{\prime})$.
The converse direction is similar. By monotonicity and naturality of $\lambda$
we obtain

$\gamma(u)\in\lambda_{\mathbb{X}}(a_{1},\ldots,a_{n})\subseteq\lambda_{\mathbb{X}}(f^{-1}(f[a_{1}]),\ldots,f^{-1}(f[a_{n}]))=(\mathsf{T}f)^{-1}(\lambda_{\mathbb{Y}}(f[a_{1}],\ldots,f[a_{n}])),$

so
$(\mathsf{T}f)(\gamma(u))\in\lambda_{\mathbb{Y}}(f[a_{1}],\ldots,f[a_{n}])$.
(The $f[a_{i}]$ need not be open in $\mathbb{Y}$, but since $\lambda$ is
strong, $\lambda_{\mathbb{Y}}(f[a_{1}],\ldots,f[a_{n}])$ is defined.) Because
$f$ and $f^{\prime}$ are coalgebra morphisms and $f(u)=f^{\prime}(u^{\prime})$
we have
$(\mathsf{T}f)(\gamma(u))=\nu(f(u))=\nu(f^{\prime}(u^{\prime}))=(\mathsf{T}f^{\prime})(\gamma^{\prime}(u^{\prime}))$.
Finally, we get

$\displaystyle\gamma^{\prime}(u^{\prime})$
$\displaystyle\in(\mathsf{T}f^{\prime})^{-1}(\lambda_{\mathbb{Y}}(f[a_{1}],\ldots,f[a_{n}]))$
$\displaystyle=\lambda_{\mathbb{X}^{\prime}}((f^{\prime})^{-1}(f[a_{1}]),\ldots,(f^{\prime})^{-1}(f[a_{n}]))$
(Naturality of $\lambda$)
$\displaystyle=\lambda_{\mathbb{X}^{\prime}}(B[a_{1}],\ldots,B[a_{n}])$
(Strong monotonicity of $\lambda$)
$\displaystyle\subseteq\lambda_{\mathbb{X}^{\prime}}(a_{1}^{\prime},\ldots,a_{n}^{\prime}).$
(Coherence of $(a_{i},a_{i}^{\prime})$)

This proves the proposition.

######  Remark 47.

If $\mathbf{C}=\mathbf{KHaus}$ in the proposition above, then Proposition 12
allows us to drop the assumption that $\Lambda$ be strong.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{Top}$ and let $\Lambda$ be a
geometric modal signature for $\mathsf{T}$. The following diagram summarises
the results from Propositions 43 and 46 and Theorem 40. The arrows indicate
that one form of equivalence implies the other. Here (1) holds if $\mathsf{T}$
preserves weak pullbacks, (2) is true when $\Lambda$ is Scott-continuous and
characteristic and $\mathsf{T}$ preserves sobriety (cf. Theorem 40), and (3)
holds when $\Lambda$ is strongly monotone. Note that the converse of (2)
always holds, because morphisms preserve truth (Proposition 9).

${{\leftrightarroweq}}$${{\leftrightarroweq_{\Lambda}}}$${{\equiv_{\Lambda}}}$${{\simeq_{\mathbf{Mod}(\mathsf{T})}}}$(2)(1)(3)
(16)

As stated in the introduction we are not only interested in endofunctors on
$\mathbf{Top}$, but also in endofunctors on full subcategories of
$\mathbf{Top}$, in particular $\mathbf{KHaus}$.

The implications in the diagram hold for endofunctors on $\mathbf{Sob}$ as
well (use Remark 41). Moreover, with some extra effort it can be made to work
for endofunctors on $\mathbf{KSob}$ as well. In order to achieve this, we have
to redo the proof for the bi-implication between modal equivalence and
behavioural equivalence. This is the content of the following theorem.

######  Theorem 48.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{KSob}$, $\Lambda$ a Scott-
continuous characteristic geometric modal signature for $\mathsf{T}$ and
$\mathfrak{X}=(\mathbb{X},\gamma,V)$ and
$\mathfrak{X}^{\prime}=(\mathbb{X}^{\prime},\gamma^{\prime},V^{\prime})$ two
geometric $\mathsf{T}$-models. Then
${\equiv_{\Lambda}}=\,{\simeq_{\mathbf{Mod}(\mathsf{T})}}$.

######  Proof 8.5.

If $x$ and $x^{\prime}$ are behaviourally equivalent then they are modally
equivalent by Proposition 9. The converse direction can be proved using
similar reasoning as in Section 7. The major difference is the following: We
define an equivalence relation $\equiv_{2}$ on
$\operatorname{GML}(\Phi,\Lambda)$ by $\varphi\equiv_{2}\psi$ iff
$\llbracket\varphi\rrbracket^{\mathfrak{X}}=\llbracket\psi\rrbracket^{\mathfrak{X}}$
and
$\llbracket\varphi\rrbracket^{\mathfrak{X}^{\prime}}=\llbracket\psi\rrbracket^{\mathfrak{X}^{\prime}}$.
(Note that $\mathfrak{X}$ and $\mathfrak{X}^{\prime}$ are now fixed.) That is,
$\varphi\equiv_{2}\psi$ iff $\varphi$ and $\psi$ are satisfied by precisely
the same states in $\mathfrak{X}$ and $\mathfrak{X}^{\prime}$ (compare
Definition 7). The frame
$\mathbf{E}_{2}:=\operatorname{GML}(\Phi,\Lambda)/{\equiv_{2}}$ can then be
shown to be a compact frame and hence
$\mathbb{Z}_{2}:=\mathsf{pt}\mathbf{E}_{2}$ is a compact sober space. The
remainder of the proof is analogous to the proof of Theorem 40. A detailed
proof can be found in [16, Theorem 3.34].

We summarise the results for $\mathbf{Top}$ and two of its full subcategories:

######  Theorem 49.

Let $\mathsf{T}$ be an endofunctor on $\mathbf{Top}$, $\mathbf{Sob}$ or
$\mathbf{KSob}$ and $\Lambda$ a Scott-continuous characteristic strongly
monotone geometric modal signature for $\mathsf{T}$. If $x$ and $x^{\prime}$
are two states in two geometric $\mathsf{T}$-models, then

$x\leftrightarroweq_{\Lambda}x^{\prime}\quad\text{iff}\quad
x\equiv_{\Lambda}x^{\prime}\quad\text{iff}\quad
x\simeq_{\mathbf{Mod}(\mathsf{T})}x^{\prime}.$

##  9\. Conclusion

We have started building a framework for coalgebraic _geometric_ logic and we
have investigated examples of concrete functors. There are still many
unanswered and interesting questions. We outline possible directions for
further research.

Modal equivalence versus behavioural equivalence:

From Theorem 49 we know that modal equivalence and behavioural equivalence
coincide in $\mathbf{Mod}(\mathsf{T})$ if $\mathsf{T}$ is an endofunctor on
$\mathbf{KSob}$, $\mathbf{Sob}$ or an endofunctor on $\mathbf{Top}$ which
preserves sobriety. A natural question is whether the same holds when
$\mathsf{T}$ is an endofunctor on $\mathbf{KHaus}$.

When does a lifted functor restrict to $\mathbf{KHaus}$?:

We know of two examples, namely the powerset functor with the box and diamond
lifting, and the monotone functor on $\mathbf{Set}$ with the box and diamond
lifting, where the lifted functor on $\mathbf{Top}$ restricts to
$\mathbf{KHaus}$. It would be interesting to investigate whether there are
explicit conditions guaranteeing that the lift of a functor restricts to
$\mathbf{KHaus}$. These conditions could be either for the
$\mathbf{Set}$-functor one starts with, or the collection of predicate
liftings for this functor, or both.

Bisimulations:

In [3] the authors define $\Lambda$-bisimulations (which are inspired by [15])
between $\mathbf{Set}$-coalgebas. In this paper we define
$\Lambda$-bisimulations between $\mathbf{C}$-coalgebras. A similar definition
yields a notion of $\Lambda$-bisimulation between $\mathbf{Stone}$-coalgebras,
where the interpretants of the proposition letters are clopen sets, see [16,
Definition 2.19]. This raises the question whether a more uniform treatment of
$\Lambda$-bisimulations is possible, which encompasses all these cases.

Modalities and finite observations:

Geometric logic is generally introduced as the logic of finite observations,
and this explains the choice of connectives ($\land$, $\bigvee$ and, in the
first-order version, $\exists$). We would like to understand to which degree
_modalities_ can safely be added to the base language, without violating the
(semantic) intuition of finite observability. Clearly there is a connection
with the requirement of _Scott-continuity_ (preservation of directed joins),
and we would like to make this connection precise, specifically in the
topological setting.

## References

  * [1] S. Abramsky.  Domain Theory and the Logic of Observable Properties.  PhD thesis, University of London, 1987.
  * [2] J. Adámek, H. Herrlich, and G.E. Strecker.  Abstract and Concrete Categories : The Joy of Cats.  Wiley, New York, 1990.
  * [3] Z. Bakhtiari and H.H. Hansen.  Bisimulation for weakly expressive coalgebraic modal logics.  In 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017, June 12-16, 2017, Ljubljana, Slovenia, pages 4:1–4:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [4] B. Banaschewski and C.J. Mulvey.  Stone-Čech compactifications of locales I.  Houston Journal of Mathematics, 6(3):301–312, 1980.
  * [5] G. Bezhanishvili, N. Bezhanishvili, and J. Harding.  Modal compact Hausdorff spaces.  Journal of Logic and Computation, 25(1):1–35, 2015.
  * [6] N. Bezhanishvili, S. Enqvist, and J. de Groot.  Duality for Instantial Neighbourhood Logic via coalgebra, 2020.  To appear in _Coalgebraic Methods in Computer Science_.
  * [7] N. Bezhanishvili, G. Fontaine, and Y. Venema.  Vietoris bisimulations.  Journal of Logic and Computation, 20(5):1017–1040, 2010.
  * [8] S. Burris and H.P. Sankappanavar.  A Course in Universal Algebra.  Springer, 1981.
  * [9] S. Celani and R. Jansana.  Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic.  Logic Journal of the IGPL, 7:683–715, 12 1999.
  * [10] B.F. Chellas.  Modal Logic: An Introduction.  Cambridge University Press, Cambridge, 1980.
  * [11] L.-T. Chen and A. Jung.  On a categorical framework for coalgebraic modal logic.  Electronic Notes in Theoretical Computer Science, 308:109–128, 2014\.
  * [12] C. Cirstea, A. Kurz, D. Pattinson, L. Schröder, and Y. Venema.  Modal logics are coalgebraic.  In S. Abramsky, E. Gelenbe, and V. Sassone, editors, Visions of Computer Science, BCS International Academic Research Conference (BCS 2008), pages 129–140. British Computer Society, 2008.
  * [13] J.M. Dunn.  Positive modal logic.  Studia Logica, 55:301–317, 1995.
  * [14] S. Enqvist and S. Sourabh.  Bisimulations for coalgebras on Stone spaces.  Journal of Logic and Computation, 28(6):991–1010, 2018.
  * [15] D. Gorín and L. Schröder.  Simulations and bisimulations for coalgebraic modal logics.  In R. Heckel and S. Milius, editors, 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, pages 253–266. Springer, 2013\.
  * [16] J. de Groot.  Coalgebraic geometric logic.  Master’s thesis, University of Amsterdam, available at https://esc.fnwi.uva.nl/thesis/centraal/files/f2119048545.pdf.
  * [17] H.H. Hansen.  Monotonic modal logics, 2003.  Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam.
  * [18] H.H. Hansen and C. Kupke.  A coalgebraic perspective on monotone modal logic.  Electronic Notes in Theoretical Computer Science, 106:121–143, 2004\.
  * [19] H.H. Hansen, C. Kupke, and E. Pacuit.  Neighbourhood structures: bisimilarity and basic model theory.  Logical Methods in Computer Science, 5(2), April 2009.
  * [20] P.T. Johnstone.  Stone Spaces.  Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.
  * [21] P.T. Johnstone.  Vietoris locales and localic semilattices.  In R.-E. Hoffmann and K.H. Hofmann, editors, Continuous lattices and their applications, Lecture Notes in Pure and Applied Mathematics, pages 155–180. Dekker, New York, 1985.  Proceedings of a conference held at the University of Bremen, July 2-3, 1982.
  * [22] P.T. Johnstone.  Sketches of an Elephant: A Topos Theory Compendium.  Number v. 2 in Oxford Logic Guides. Clarendon Press, 2002.
  * [23] P.T. Johnstone and S.J. Vickers.  Preframe representations present.  In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory: Proceedings of the International Conference held in Como, Italy, July 22-28, 1990, Lecture Notes in Mathematics, pages 193–212. Springer Berlin Heidelberg, 2006.
  * [24] B. Klin.  Coalgebraic modal logic beyond sets.  Electronic Notes in Theoretical Computer Science, 173:177 – 201, 2007.  Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII).
  * [25] C. Kupke, A. Kurz, and D. Pattinson.  Algebraic semantics for coalgebraic logics.  Electronic Notes in Theoretical Computer Science, 106:219–241, 2004\.  Proceedings of the Workshop on Coalgebraic Methods in Computer Science (CMCS).
  * [26] C. Kupke, A. Kurz, and D. Pattinson.  Ultrafilter extensions for coalgebras.  In J. Luiz Fiadeiro, N. Harman, M. Roggenbach, and J. Rutten, editors, Algebra and Coalgebra in Computer Science, pages 263–277, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
  * [27] C. Kupke, A. Kurz, and Y. Venema.  Stone coalgebras.  Theoretical Computer Science, 327(1):109–134, 2004.  Selected Papers of CMCS ’03.
  * [28] C. Kupke and D. Pattinson.  Coalgebraic semantics of modal logics: An overview.  Theoretical Computer Science, 412(38):5070–5094, 2011.  CMCS Tenth Anniversary Meeting.
  * [29] S.M. Lane.  Categories for the Working Mathematician.  Graduate Texts in Mathematics. Springer New York, 1971.
  * [30] E. Michael.  Topologies on spaces of subsets.  Transactions of the American Mathematical Society, 71:152–182, 1951\.
  * [31] L.S. Moss.  Coalgebraic logic.  Annals of Pure and Applied Logic, 96(1):277–317, 1999.
  * [32] D. Pattinson.  Coalgebraic modal logic: soundness, completeness and decidability of local consequence.  Theoretical Computer Science, 309(1):177–193, 2003.
  * [33] J. Picado, A. Pultr, and A. Tozzi.  Locales.  In M. Pedicchio and W. Tholen, editors, Categorical Foundations, volume 97 of Encyclopedia of Mathematics and its Applications, pages 49–101. Cambridge University Press, 2004.
  * [34] J.J.M.M. Rutten.  Universal coalgebra: a theory of systems.  Theoretical Computer Science, 249((1)):3–80, 2000.
  * [35] L. Schröder.  Expressivity of coalgebraic modal logic: The limits and beyond.  In V. Sassone, editor, Foundations of Software Science and Computational Structures, pages 440–454, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
  * [36] Y. Venema.  Coalgebra and modal logic, 2017.  Course notes. ILLC, UvA.
  * [37] Y. Venema, S. Vickers, and J. Vosmaer.  Generalized powerlocales via relation lifting.  CoRR, abs/1202.3264, 2012.
  * [38] Y. Venema, S.J. Vickers, and J. Vosmaer.  Generalised powerlocales via relation lifting.  Mathematical Structures in Computer Science, 23(1):142–199, 2013\.
  * [39] S.J. Vickers.  Topology via Logic.  Cambridge University Press, New York, NY, USA, 1989.