Neighbourhood Coalgebras

(draft)

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\looparrowright 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:Ord\to Set$ is left-adjoint to the discrete functor $D:Set\to Ord$. 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 D2^{2^{CX}}$.

Remark: The function $f:X\to Y$ in $Set$ ^[1] is a coalgebra morphism from $\xi:X\to 2^{2^X}$ to $\nu:Y\to 2^{2^Y}$ iff

Remark: Similarly, $R$ is a bisimulation if $xRy$ implies

References¶

Hansen, Kupke, Pacuit: Neighbourhood Structures: Bisimilarity and Basic Model Theory. 2009. (Definition 2.1., ...)

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