Neighbourhood Coalgebras

(draft) … (up)

The idea of the following is to run through (Hansen, Kupke, Pacuit, 2009) and analyse it from the point of view of cospan bisimulation.

Def: Let

R \subseteq X \times Y

. The dual relation

R^{\partial} : 2^{X} ↬ 2^{Y}

is defined by

R [a] \subseteq b

Remark:

(a, b)

are called

R

-coherent in Def 2.1 of Hansen-Kupke-Pacuit if

(a, b) \in R^{\partial}

and

(b, a) \in (R^{- 1})^{\partial}

Recall that the connected component functor

C : O r d \to S e t

is left-adjoint to the discrete functor

D : S e t \to O r d

. Also recall that the ordification of the neighbourhood functor is $D2^{2{C-}}, see Theorem 8 in [DK17] and the section on Cospan Bisimulation.

Definition: A neighbourhood frame is a set

X

with a function

X \to 2^{2^{X}}

. An ordered neighbourhood frame is an ordered set

X

with an order-preserving function

X \to D 2^{2^{C X}}

Remark: The function

f : X \to Y

S e t

^[1] is a coalgebra morphism from

ξ : X \to 2^{2^{X}}

ν : Y \to 2^{2^{Y}}

iff

\begin{matrix} \forall a \in ξ (x) . \exists b \in ν (y) . (\forall x \in a . \exists y \in b . f x = y) & (\forall y \in b . \exists x \in a . f x = y) \\ \forall b \in ν (y) . \exists a \in ξ (x) . (\forall x \in a . \exists y \in b . f x = y) & (\forall y \in b . \exists x \in a . f x = y) \end{matrix}

Remark: Similarly,

R

is a bisimulation if

x R y

implies

\begin{matrix} \forall a \in ξ (x) . \exists b \in ν (y) . (\forall x \in a . \exists y \in b . x R y) & (\forall y \in b . \exists x \in a . x R y) \\ \forall b \in ν (y) . \exists a \in ξ (x) . (\forall x \in a . \exists y \in b . x R y) & (\forall y \in b . \exists x \in a . x R y) \end{matrix}

References

Dahlqvist and Kurz: The Positivication of Coalgebraic Logics. CALCO 2017. (Section 3.3 and 3.4)