---
tag: JCCTFJV9CN
kind: definition
name: Homotopy type theory
msc: ["03B38", "55U35", "03F55"]
defines: EPAAKD80H9
uses: [KCV8RKBATN, ESVYD9CZ8C, 0XHDTE5YMZ]
sources:
  - url: https://en.wikipedia.org/wiki/Homotopy_type_theory
---

## Definition

Start from [[intuitionistic type theory|KCV8RKBATN]] with intensional identity types, dependent function and pair types, and a hierarchy of universes.
*Homotopy type theory* is this theory extended by two principles.

1. The *univalence axiom*: for each universe $U$ and all types $A, B : U$, the canonical map $\mathrm{idtoeqv} \colon (A =_U B) \to (A \simeq B)$ is an equivalence.
2. *Higher inductive types*: types given by generators for points and also for paths. An example is the circle $S^1$, generated by a point $\mathrm{base} : S^1$ and a path $\mathrm{loop} : \mathrm{base} =_{S^1} \mathrm{base}$.

Here $A \simeq B$ is the type of equivalences, that is, of functions $f \colon A \to B$ that have a two-sided inverse up to identification.
The theory is read homotopically.
A type is a space, a term $a : A$ is a point, and a term $p : a =_A b$ is a path from $a$ to $b$.

## Remarks

Example: in homotopy type theory one proves that the type of loops $\mathrm{base} =_{S^1} \mathrm{base}$ is equivalent to the integers $\Z$.
This matches the classical fact that the fundamental group of the circle is $\Z$.
Non-example: intuitionistic type theory with extensional identity types, where any two terms of $a =_A b$ are equal, is not compatible with univalence.
The type $\mathbf{2}$ of booleans has two self-equivalences, the identity and the swap.
With univalence they give two paths $\mathbf{2} = \mathbf{2}$, and extensional identity types make these paths equal.
Then the identity and the swap would be equal, which is false.
Univalence implies function extensionality: two [[functions|0XHDTE5YMZ]] that agree at each point are equal.