# Homotopy Type Theory homotopy groups

## Idea

Since paths in a space $X$ 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 $X$.

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

## Definition

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

$\pi_n(X,x) := \| \Omega^n (X, x) \|_0$

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

## Properties

TODO: Expand this out

• $\pi_n(X \times Y) \simeq \pi_n(X) \times \pi_n(Y)$

• If $X$ is $n$-truncated? then $\pi_k(X)=1$ for all $k \gt n$.

• If $X$ is $n$-connected? then $\pi_k(X)=1$ for all $k \lt n$.