# Commit 2022-07-19 01:02 3600b621

View on Github →feat(topology/homotopy): define nth homotopy group πₙ (without the group instance) (#14724) This pull request adds:

- definition of the nth homotopy group
`π n x`

- proof of
`π 0 x ≃ zeroth_homotopy X`

where`x:X`

- proof of
`π 1 x ≃ path.homotopic.quotient x x`