nLab
(-1)-groupoid

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

Definition

A (1)(-1)-groupoid or (-1)-type is a truth value, or equivalently an (−1)-truncated object in ∞Grpd. By excluded middle, this is either the empty groupoid (false) or the terminal groupoid (true, the point).

Remarks

Compare the concept of 0-groupoid (a set) and (−2)-groupoid (which is trivial). The point of (1)(-1)-groupoids is that they complete some patterns in the periodic table of nn-categories. (They also shed light on the theory of homotopy groups and n-stuff.)

For example, there should be a 00-category of (1)(-1)-groupoids; a 00-category is also a set, and this set is the set of truth values: classically

(1)Grpd:={,} (-1)Grpd := \{\bot, \top\}

Actually, since for other values of nn, n-groupoids form not just an (n+1)(n+1)-category but an (n+1,1)(n+1,1)-category, we should expect the 00-category of (1)(-1)-groupoids to be a (0,1)(0,1)-category, or 11-poset. This simply means a poset, and indeed truth values do always form a poset, classically (\bot \leq \top).

If we equip the category of (1)(-1)-groupoids with the monoidal structure of conjunction (the logical AND operation), then a groupoid enriched over this is a setoid, and a category enriched over it is a proset. Up to equivalence of categories, these are the same as a set (a 00-groupoid) and a poset (a (0,1)-category); this fits the patterns of the periodic table.

See (−1)-category for more on this sort of negative thinking.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/unit type/contractible type
h-level 1(-1)-truncated(-1)-groupoid/truth valuemere proposition, h-proposition
h-level 20-truncateddiscrete space0-groupoid/setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/groupoid(2,1)-sheaf/stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoidh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoidh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoidh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/∞-stackh-\infty-groupoid

Revised on September 10, 2012 20:22:24 by Urs Schreiber (131.174.188.17)