Homotopy Type Theory Boolean dagger 2-poset > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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 functional dagger monomorphism 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

  • The unitary isomorphism classes of functional dagger monomorphisms into every object AA is a Boolean algebra?. Since every functional dagger monomorphism is a map, the category of maps is a Boolean category?.

Examples

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

See also

Revision on April 21, 2022 at 14:09:56 by Anonymous?. See the history of this page for a list of all contributions to it.