# nLab Boolean dagger 2-poset

### Context

#### Higher category theory

higher category theory

## Idea

A Boolean dagger 2-poset is a dagger 2-poset whose category of maps is a Boolean category.

## Definition

A Boolean dagger 2-poset $C$ is a Heyting dagger 2-poset where for each objects $A \in Ob(C)$, $B \in Ob(C)$ and monic map $i_{B,A} \in Hom(B,A)$, there is a unitary isomorphism $j_{B,A} \in A \cong^\dagger B \cup (B \Rightarrow 0)$.

## Examples

The dagger 2-poset of sets with decidable equality and relations is an Boolean dagger 2-poset.