---
tags: coalgebraic logic
---
# Logic of Ordered Neighbourhood Coalgebras

(draft ... references to be added) ... ([up](https://hackmd.io/@alexhkurz/ryrkkYZZc))

## Introduction

We write $2$ for the 2-chain $0<1$ in various ordered categories such as posets or bounded distributed lattices.

Let
- $U:Pos\to Pos$ take upsets ordered by reverse inclusion: $UX=[X,2]^o$
- $D:Pos\to Pos$ take downsets ordered by inclusion: $DX=[X^o,2]$

Let

- $\mathcal X$ be the category of poset
- $\mathcal A$ be the category of bounded distributive lattices
- $T=DU$

Then $Coalg(T)$ is category of (monotone) neighbourhood frames (over posets). In particular $DUX=Up\mathcal PX$ for discrete $X$. Note that $DUX=2^{2^X}$ if we define $2^X$ as the poset of monotone maps $X\to 2$.

Let
- $P:\mathcal X\to\mathcal A$ be the contravariant functor $X\mapsto 2^X$.
- $S:\mathcal A\to\mathcal X$ the contravariant functor $A\mapsto DL(A,2)$.

Then
- the dual $U^\partial:DL\to DL$ of $U$ is presented by operations and equations as follows. $U^\partial A$ is generated by $\{\Box a\mid a\in PX\}$ and the equations stating that $\Box$ preserves finite meets. This gives an isomorphism
$$ U^\partial PX\to UPX$$

for finite posets $X$.

- the dual $D^\partial:DL\to DL$ of $D$ is presented by operations and equations as follows. $D^\partial A$ is generated by $\{\Diamond a\mid a\in PX\}$ and the equations stating that $\Diamond$ preserves finite meets. This gives an isomorphism
$$ D^\partial PX\to DPX$$

for finite posets $X$.

## The 2-sorted view

We can also think of coalgebras
$$X \to UDX$$

as special 2-dimensional coalgebras
$$(X,Y) \to (UY,DX).$$

The dual of these coalgebras on the algebraic side are algebras

$$(D^\partial B,U^\partial A)\to (A,B)$$

**Remark:** Given functors $F$ and $G$, [Kurz-Petrisan](https://alexhkurz.github.io/papers/cmcs08-j.pdf) calls the functor which maps $(X,Y)$ to $(FY,GX)$ the symmetric composition of $F$ and $G$. While the presentation of the functor $FG$ is typically not compositional in the presentations of $F$ and $G$, the symmetric composition does have the obvious componentwise presentation.

## An adjunction

Let $Coalg(F,G)$ be the category of 2-sorted coalgebras of the kind
$$(X,Y)\to (FY,GX).$$

**Theorem**: $Coalg(FG)$ is a full reflective subcategory of $Coalg(F,G)$.

*Proof*: We map $X\to FGX$ to $(X,GX)\to (FGX,GX)$ where the second component is the identity. This functor has a left adjoint which maps $(X,Y)\to (FY,GX)$ to $X\to FY\to FGX$.

The unit of the adjunction is the obvious coalgebra morphism from $(X,Y)\to (FY,GX)$ to $(X,GX)\to (FGX,GX)$. The counit is the identity.

Moreover, the right-adjoint is full and faithful. QED

**Corollary**: $Coalg(FG)$ is closed under limits in $Coalg(F,G)$. In particular, the final coalgebra in $Coalg(F,G)$ is also the final coalgebra in $Coalg(FG)$.

**Corollary:** $Alg(FG)$ is a full co-reflective subcategory of $Alg(F,G)$.

**Corollary**: The category of $D^\partial U^\partial$-algebras is a full coreflective subcategory of $Alg(D^\partial, U^\partial)$.

**Corollary**: $Alg(FG)$ is closed under colimits in $Alg(F,G)$. In particular, the initial algebra in $Alg(F,G)$ is also the initial algebra in $Alg(FG)$.

## References

Pauly: ...

Hansen, Kupke: ...

Kurz, Petrisan: ...

...