nLab homotopy


This page is about homotopy as a transformation. For homotopy sets in homotopy categories, see homotopy (as an operation).


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
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit 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 setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
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




In many categories CC in which one does homotopy theory, there is a notion of homotopy between morphisms, which is closely related to the 2-morphisms in higher category theory: a homotopy between two morphisms is a way in which they are equivalent.

If we regard such a category as a presentation of an (,1)(\infty,1)-category, then homotopies fgf\sim g present the 2-cells fgf\Rightarrow g in the resulting (,1)(\infty,1)-category.


In topological spaces


For f,g:XYf,g\colon X \longrightarrow Y two continuous functions between topological spaces X,YX,Y, then a left homotopy

η:f Lg \eta \colon f \,\Rightarrow_L\, g

is a continuous function

η:X×IY \eta \;\colon\; X \times I \longrightarrow Y

out of the standard cylinder object over XX: the product space of XX with the Euclidean closed interval I[0,1]I \coloneqq [0,1], such that this fits into a commuting diagram of the form

X (id,δ 0) f X×I η Y (id,δ 1) g X. \array{ X \\ {}^{\mathllap{(id,\delta_0)}}\downarrow & \searrow^{\mathrlap{f}} \\ X \times I &\stackrel{\eta}{\longrightarrow}& Y \\ {}^{\mathllap{(id,\delta_1)}}\uparrow & \nearrow_{\mathrlap{g}} \\ X } \,.

(graphics grabbed from J. Tauber here)


Let XX be a topological space and let x,yXx,y \in X be two of its points, regarded as functions x,y:*Xx,y \colon \ast \longrightarrow X from the point to XX. Then a left homotopy, def. , between these two functions is a commuting diagram of the form

* δ 0 x I η X δ 1 y *. \array{ \ast \\ {}^{\mathllap{\delta_0}}\downarrow & \searrow^{\mathrlap{x}} \\ I &\stackrel{\eta}{\longrightarrow}& X \\ {}^{\mathllap{\delta_1}}\uparrow & \nearrow_{\mathrlap{y}} \\ \ast } \,.

This is simply a continuous path in XX whose endpoints are xx and yy.

In enriched categories

If CC is enriched over Top, then a homotopy in CC between maps f,g:XYf,g:X\,\rightrightarrows \,Y is a map H:[0,1]C(X,Y)H:[0,1] \to C(X,Y) in TopTop such that H(0)=fH(0)=f and H(1)=gH(1)=g. In TopTop itself this is the classical notion.

If CC has copowers, then an equivalent definition is a map [0,1]XY[0,1]\odot X\to Y, while if it has powers, an equivalent definition is a map X([0,1],Y)X\to \pitchfork([0,1],Y).

There is a similar definition in a simplicially enriched category, replacing [0,1][0,1] with the 1-simplex Δ 1\Delta^1, with the caveat that in this case not all simplicial homotopies need be composable even if they match correctly. (This depends on whether or not all (2,1)-horns in the simplicial set, C(X,Y)C(X,Y), have fillers.) Likewise in a dg-category we can use the “chain complex interval” to get a notion of chain homotopy.

In model categories

If 𝒞\mathcal{C} is a model category, it has an intrinsic notion of homotopy determined by its factorizations. For more on the following see at homotopy in a model category.


Let 𝒞\mathcal{C} be a model category and X𝒞X \in \mathcal{C} an object.

  • A path object Path(X)Path(X) for XX is a factorization of the diagonal X:XX×X\nabla_X \colon X \to X \times X as
X:XWiPath(X)(p 0,p 1)X×X. \nabla_X \;\colon\; X \underoverset{\in W}{i}{\longrightarrow} Path(X) \overset{(p_0,p_1)}{\longrightarrow} X \times X \,.

where XPath(X)X\to Path(X) is a weak equivalence. This is called a good path object if in addition Path(X)X×XPath(X) \to X \times X is a fibration.

  • A cylinder object Cyl(X)Cyl(X) for XX is a factorization of the codiagonal (or “fold map”) Δ X:XXX\Delta_X: X \sqcup X \to X as
Δ X:XX(i 0,i 1)Cyl(X)pWX. \Delta_X \;\colon\; X \sqcup X \overset{(i_0,i_1)}{\longrightarrow} Cyl(X) \underoverset{p}{\in W}{\longrightarrow} X \,.

where Cyl(X)XCyl(X) \to X is a weak equivalence. This is called a good cylinder object if in addition XXCyl(X)X \sqcup X \to Cyl(X) is a cofibration.


By the factorization axioms every object in a model category has both a good path object and as well as a good cylinder object according to def. . But in some situations one is genuinely interested in using non-good such objects.

For instance in the classical model structure on topological spaces, the obvious object X×[0,1]X\times [0,1] is a cylinder object, but not a good cylinder unless XX itself is cofibrant (a cell complex in this case).

More generally, the path object Path(X)Path(X) of def. is analogous to the powering (I,X)\pitchfork(I,X) with an interval object and the cylinder object Cyl(X)Cyl(X) is analogous to the tensoring IXI\odot X with an interval object. In fact, if 𝒞\mathcal{C} is a VV-enriched model category and XX is fibrant/cofibrant, then these powers and copowers are in fact examples of (good) path and cylinder objects if the interval object is sufficiently good.


Let f,g:XYf,g \colon X \longrightarrow Y be two parallel morphisms in a model category.

  • A left homotopy η:f Lg\eta \colon f \Rightarrow_L g is a morphism η:Cyl(X)Y\eta \colon Cyl(X) \longrightarrow Y from a cylinder object of XX, def. , such that it makes this diagram commute:
X Cyl(X) X f η g Y. \array{ X &\longrightarrow& Cyl(X) &\longleftarrow& X \\ & {}_{\mathllap{f}}\searrow &\downarrow^{\mathrlap{\eta}}& \swarrow_{\mathrlap{g}} \\ && Y } \,.
  • A right homotopy η:f Rg\eta \colon f \Rightarrow_R g is a morphism η:XPath(Y)\eta \colon X \to Path(Y) to some path object of XX, def. , such that this diagram commutes:
X f η g Y Path(Y) Y. \array{ && X \\ & {}^{\mathllap{f}}\swarrow & \downarrow^{\mathrlap{\eta}} & \searrow^{\mathrlap{g}} \\ Y &\longleftarrow& Path(Y) &\longrightarrow& Y } \,.

By remark it follows that in a TopTop-enriched model category, any enriched homotopy between maps XYX\to Y is a left homotopy if XX is cofibrant and a right homotopy if YY is fibrant. Similar remarks hold for other enrichments.

For more see at homotopy in a model category.

In (co-)fibration categories

Clearly the concept of left homotopy in def. only needs part of the model category axioms and thus makes sense more generally in suitable cofibration categories. Dually, the concept of path objects in def. makes sense more generally in suitable fibration categories such as categories of fibrant objects in the sense of Brown.

Likewise if there is a cylinder functor, one gets functorially defined cylinder objects, etc.

In Martin-Löf dependent type theory

In Martin-Löf dependent type theory, let f,g: (x:A)P(x)f,g : \prod_{(x:A)}P(x) be two terms of a dependent product type of a type family P:A𝒰P: A \to \mathcal{U}. A homotopy from ff to gg is a dependent function? of type

(fg) x:A(f(x)=g(x))(f \sim g) \equiv \prod_{x : A} (f(x) = g(x))

Note that a homotopy is not the same as an identification f=gf = g. However this can be made so if one assumes function extensionality.

[S n,][S^n,-][,A][-,A]()A(-) \otimes A
category theorycovariant homcontravariant homtensor product
homological algebraExtExtTor
enriched category theoryendendcoend
homotopy theoryderived hom space Hom(S n,)\mathbb{R}Hom(S^n,-)cocycles Hom(,A)\mathbb{R}Hom(-,A)derived tensor product () 𝕃A(-) \otimes^{\mathbb{L}} A


See the references at homotopy theory and at model category.

Discussion in computational topology:

For homotopies in Martin-Löf dependent type theory:

Last revised on June 9, 2022 at 20:31:39. See the history of this page for a list of all contributions to it.