nLab Boolean dagger 2-poset

Context

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

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 CC is a Heyting dagger 2-poset where for each objects AOb(C)A \in Ob(C), BOb(C)B \in Ob(C) and monic map i B,AHom(B,A)i_{B,A} \in Hom(B,A), there is a unitary isomorphism j B,AA B(B0)j_{B,A} \in A \cong^\dagger B \cup (B \Rightarrow 0).

Properties

Examples

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

See also

Created on May 3, 2022 at 22:07:14. See the history of this page for a list of all contributions to it.