Contents

Idea

A 0-groupoid or 0-type a set. This terminology may seem strange at first, but it is very helpful to see sets as the beginning of a sequence of concepts: sets, groupoids, 2-groupoids, 3-groupoids, etc. Doing so reveals patterns such as the periodic table. (It also sheds light on the theory of homotopy groups and n-stuff.)

For example, there should be a $1$-groupoid of $0$-groupoids; this is the underlying groupoid of the category of sets. Then a groupoid enriched over this is a $1$-groupoid (more precisely, a locally small groupoid). Furthermore, an enriched category is a category (or $1$-category), so a $0$-groupoid is the same as a 0-category.

One can continue to define a (−1)-groupoid to be a truth value and a (−2)-groupoid to be a triviality (that is, there is exactly one).

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+2$$n$-truncatedhomotopy n-typen-groupoidh-$n$-groupoid
h-level $\infty$untruncatedhomotopy type∞-groupoid(∞,1)-sheaf/∞-stackh-$\infty$-groupoid

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