Homotopy Type Theory Boolean dagger 2-poset > history (Rev #5)

Contents

Idea

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

Definition

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

Properties

Examples

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

See also

Revision on April 25, 2022 at 10:39:15 by Anonymous?. See the history of this page for a list of all contributions to it.