Homotopy Type Theory W-topical dagger 2-poset > history (Rev #2, changes)

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

Contents

Idea

A W-topical dagger 2-poset is a dagger 2-poset whose category of maps is a W-topos?.

Definition

A W-topical dagger 2-poset CC is an elementarily topical dagger 2-poset with an object :Ob(C)\mathbb{N}:Ob(C) and maps 0:Hom(𝒫(0),𝒩)0:Hom(\mathcal{P}(0),\mathcal{N}) and s:Hom(,)s:Hom(\mathbb{N},\mathbb{N}), such that for every object AA with maps 0 A:Hom(𝒫(0),A)0_A:Hom(\mathcal{P}(0),A) and s A:Hom(A,A)s_A:Hom(A,A), there is a map f:Hom(,A)f:Hom(\mathbb{N},A) such that f0=0 Af \circ 0 = 0_A and fs=s Aff \circ s = s_A \circ f.

Examples

The dagger 2-poset of sets and relations is a W-topical dagger 2-poset.

See also

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