Homotopy

Homotopies, a key player of topology and the central object of homotopy theory, are continuous deformations between functions. A homotopy between functions $f$ and $g$ is denoted $H:f\sim g$.[cite:@rijke2022introduction]

Homotopy in homotopy type theory

In homotopy type theory, homotopies encode the commutativity of diagrams. For example, the triangle

commutes iff it is equipped with a homotopy $H:f\sim gh$.

The definition of homotopy used in Agda's cubical library couldn't be more on the nose about this:

  _∼_ : {X : Type ℓ} {Y : X → Type ℓ'} → (f g : (x : X) → Y x) → Type (ℓ-max ℓ ℓ')
  _∼_ {X = X} f g = (x : X) → f x ≡ g x

Homotopy between paths

A homotopy $H:\text{intI}\times \text{intI}\to X$ between paths $p,q:\text{intI}\to X$ is a two-dimensional map and can be regarded as a path between paths.Proposing the idea of paths between paths begs the question "what about paths between paths between paths?" This leads us to "(weak) ∞-groupoids," an algebraic structure with a collection of objects, a collection of morphisms between objects, a collection of morphisms between morphisms between objects, and so on, with each "layer" of morphisms additionally bearing a bit of algebraic structure: associativity, identity, and inverses. One can informally visualise the image of $H$ as "filling the space" between $p$ and $q$, but this does not generally hold up.[cite:@hottbook]