nLab Boolean dagger 2-poset

Contents

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)$.

Properties

• The isomorphism classes of monic maps into every object $A$ is a Boolean algebra. Since every monic map is a map, the category of maps is a Boolean category.

Examples

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

See also

• dagger 2-poset
• coherent dagger 2-poset
• geometric dagger 2-poset
• Heyting dagger 2-poset
• Boolean dagger 2-poset
• Boolean topical dagger 2-poset