Homotopy Type Theory
homotopy groups


Since paths in a space XX can be associatively concatenated and inverted they can form a group. For this to be a group however paths between paths need be unique making is a h-Set?. This group tells us much of the homotopical information associated with XX.

Knowing the homotopy groups of a space can tell you a great deal about many things. See homotopy group


The nnth homotopy group of a pointed space (X,x)(X, x) is defined as:

π n(X,x):=Ω n(X,x) 0\pi_n(X,x) := \| \Omega^n (X, x) \|_0

Where 0\|-\|_0 is the set-truncation?, and Ω n\Omega^n is the nn-fold iterated loop space. Note that there is not group structure (usually) when n=0n = 0, and since Ω 0:=id_X\Omega^0 := \text{id_X} it is usually ignored, and nn-assumed positive. (In classical algebraic topology, set-truncation? would be written as π 0\pi_0). It is also typically implied by the context that XX is pointed hence (X,x)(X,x) is written as XX when unambiguous.


TODO: Expand this out

  • π n(X×Y)π n(X)×π n(Y)\pi_n(X \times Y) \simeq \pi_n(X) \times \pi_n(Y)

  • If XX is nn-truncated? then π k(X)=1\pi_k(X)=1 for all k>nk \gt n.

  • If XX is nn-connected? then π k(X)=1\pi_k(X)=1 for all k<nk \lt n.

See also


Created on February 14, 2019 at 04:01:50. See the history of this page for a list of all contributions to it.