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

Showing changes from revision #5 to #6: Added | Removed | Changed



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


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



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

See also

Revision on June 6, 2022 at 20:34:00 by Anonymous?. See the history of this page for a list of all contributions to it.