nLab homotopy type



Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




Traditionally, a homotopy type is a topological space regarded up to weak homotopy equivalence, (although this may sometimes be referred to as its weak homotopy type, (see below)). Formally this may be taken to mean the object that XX represents in the standard homotopy category Ho(Top), or, better, in the (∞,1)-category ∞Grpd \simeq L wheTopL_{whe} Top, the simplicial localization of the category Top at the weak homotopy equivalences, of which Ho(Top)Ho(Top) is the decategorification. As such, topological spaces regarded as homotopy types are equivalently ∞-groupoids (see at homotopy hypothesis for more on this).

More generally, then, we may think of every object in any (∞,1)-topos 𝒞\mathcal{C} as being a homotopy type in the world of 𝒞\mathcal{C} (just as we may think of an object of a 1-topos 𝒮\mathcal{S} as being a “set in the world of 𝒮\mathcal{S}”). For instance, if 𝒞=Sh (C)\mathcal{C} = Sh_\infty(C) is an (∞,1)-category of (∞,1)-sheaves/of ∞-stacks over some (∞,1)-site CC, then an object of 𝒞\mathcal{C} may be thought of as a homotopy type over CC, or a sheaf of homotopy types. If 𝒞\mathcal{C} is the classifying topos of some geometric theory TT, then an object of 𝒞\mathcal{C} may be called a “TT-structured homotopy type”. And if 𝒞\mathcal{C} is a cohesive (∞,1)-topos, an object of 𝒞\mathcal{C} may be called a “cohesive homotopy type”. In the special case that 𝒞=Sh (*)Gprd\mathcal{C} = Sh_\infty(*) \simeq \infty Gprd, this reproduces the traditional notion.

The reason this makes sense is that any (,1)(\infty,1)-topos has an internal language, which is homotopy type theory — a formal logic whose basic objects are abstract things called homotopy types, just as the basic objects of set theory are abstract things called sets. Inside the internal logic of 𝒞\mathcal{C}, its objects behave like classical homotopy types (although the ambient logic is constructive). This explains why we can think of objects of 𝒞\mathcal{C} as “homotopy types in the world of 𝒞\mathcal{C}”: they are the categorical semantics of these abstract homotopy types in the internal logic of 𝒞\mathcal{C}. In the special case of Grpd\infty Grpd, the internal and external logic are the same, so this meaning also includes the classical usage of “homotopy type”.

Homotopy nn-types

A homotopy type that is an n-truncated object in an (∞,1)-category or equivalently that interprets a type of homotopy level n+2n+2 is also called a homotopy n-type or nn-type for short. For topological spaces / ∞-groupoids this means that all homotopy groups above degree nn are trivial.


In topological spaces

In traditional homotopy theory of topological spaces one sometimes distinguishes the notion of strong homotopy types from that of weak homotopy types, depending on whether one regards topological spaces up to homotopy equivalence or up to weak homotopy equivalence (see also there the section Relation to homotopy types).

The two notions agree on good cofibrant spaces, namely on the CW-complexes (see model structure on topological spaces) and for homotopy theory proper it is the weak homotopy equivalences that matter.

More precisely, weak homotopy equivalences between spaces give an equivalence relation on the class of topological spaces, and referring to a homotopy type means that you are to consider properties of a space that are shared by any of the spaces weakly equivalent to it and thus in that equivalence class. In this expanded sense, therefore, a homotopy type is such a weak equivalence class of spaces. Using the terminology from homotopy category, two spaces have the same homotopy type if they are isomorphic in Ho(Top).

By standard theorems, homotopy types in topological can also be ‘modeled’ by many other structures, such as

In most cases the tools of homotopy theory, in particular model categories, can be used to establish these equivalences.

The sense of ‘modeled’ is related to Whitehead’s algebraic homotopy theory. A setting such as those above acts as a model for homotopy types if there are comparison functors between Spaces\Spaces and the category, and some notion of homotopy within the category yielding an equivalence of homotopy categories.


Although the notion of homotopy type is defined for arbitrary spaces, it is most usual to restrict attention to ‘locally nice’ spaces such as polyhedra (i.e. realisations of simplicial complexes or CW-complexes). Various other classes of space occur naturally in various parts of mathematics in particular in analysis and algebraic geometry and there the methods of abstract homotopy theory provide a way of mimicking the basic idea of homotopy type as described above.


Using variants of ‘weak equivalence’, for instance, ‘nn-equivalence’, one gets coarser notions of equivalence which can be very useful. The particular case of nn-equivalence leads to the related notion of homotopy n-type.

type, type theory

dependent type, dependent type theory, Martin-Löf dependent type theory

homotopy type, homotopy type theory

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


For instance:

Last revised on January 2, 2023 at 15:13:22. See the history of this page for a list of all contributions to it.