Homotopy type theory

Homotopy type theory (HoTT) is Martin-Löf type theory adorned with higher inductive types and the Univalence axiom.

Interpretation of $\mathrm{Type}\mathrm{Type}a\text{T}A\text{Type}$

A central idea in HoTT is the many equivalent interpretations of the statement $\mathrm{Type}\mathrm{Type}a\text{T}A\text{Type}$:

• proof-theoretically, "$a$ is a proof of proposition $\text{T}A$;"

• type-theoretically, "$a$ is an object of type $\text{T}A$;"

• geometrically/categorically, "$\text{T}A$ is a space and $\text{Type}$ is the category of spaces."

Paths

The core idea of HoTT and univalent foundations is a correspondence between paths Path A x x and equalities x = y.

  refl : ∀ {ℓ} {A : Set ℓ} {x : A} → Path A x x
  refl {x = x} = λ i → x

While propositions are simply true or false, the path perspective has more structure.

While the traditional notion of equality captures merely the source and destination, the path view additionally captures the exact way you get from $A$ to $B$ — i.e. proof relevance.

In Cubical Agda, this translates to an element of type x ≡ y being a description of how to traverse a path from x to y. The "i value" tells you how far along that path we are.

See also

• Proof-relevance

• Agda

References

• https://github.com/Smaug123/CubicalTutorial