nLab (-1)-groupoid

Redirected from "(-1)-types".
Note: (-1)-groupoid and (-1)-groupoid both redirect for "(-1)-types".
Contents

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 symmetric proset, 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)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

Last revised on September 22, 2022 at 18:55:55. See the history of this page for a list of all contributions to it.