Homotopy type theory · The Lumenary

Lens

MotivationH

What does it mean to be the same?

Mathematicians routinely say "the cyclic group of order 2" or "the circle", although there are many isomorphic copies of each. Informally we identify isomorphic structures, because every property we care about is invariant under isomorphism. Formally, in ZFC, isomorphic structures are different sets, and nothing in the foundations stops us from asking non-invariant questions ("is $0 \in 1$ ?").

Homotopy type theory (HoTT) starts from a foundation in which this informal practice becomes a theorem. It builds on Martin-Löf's dependent type theory (see Type theory), in which a proof of $a = b$ is itself a mathematical object, an element of the identity type $a =_A b$ . In 1994 Hofmann and Streicher found a model in which two proofs of $a = b$ need not be equal; from 2006 onwards Awodey and Warren, and Voevodsky, saw that identity types behave exactly like path spaces in homotopy theory. Voevodsky then proposed the univalence axiom: for types $A$ and $B$ , identifications $A = B$ are the same as equivalences $A \simeq B$ . Under univalence, isomorphic structures are equal, and every construction automatically respects equivalence.

This lesson is an orientation: the path reading of identity types, univalence, higher inductive types and the computation of the loop space of the circle — and, through Lean, a precise picture of what an ordinary proof assistant can and cannot say about all this. It assumes Type theory and Algebraic topology.

IntuitionH

A dictionary

The guiding idea is a three-way dictionary between logic, sets and homotopy theory.

Type theory	Set-level reading	Homotopy reading
type $A$	set	space (∞-groupoid)
term $a : A$	element	point
$a =_A b$	proposition " $a$ equals $b$ "	space of paths from $a$ to $b$
$p : a = b$ , $q : b = c$ , $p \cdot q$	transitivity	concatenation of paths
family $P : A \to \mathcal{U}$	family of sets	fibration over $A$
$\Sigma_{x : A} P(x)$	disjoint union	total space
$\Pi_{x : A} P(x)$	product	space of sections
transport along $p$	substitution	lifting paths to the fibration
contractible type	singleton	a point (up to homotopy)

The surprise is the third row. In the homotopy reading, two elements can be equal in more than one way, and the ways themselves can be equal in more than one way, and so on: every type carries the structure of a weak ∞-groupoid (Lumsdaine; van den Berg and Garner). Types are sorted by homotopy level: contractible types; propositions (any two elements are equal); sets (any two paths between two elements are equal); groupoids; and so on.

The circle S¹ and its universal cover. In HoTT the cover is a type family code over S¹ with fibre ℤ over the base point; transport along loop moves up the helix by one step (the successor). Following a loop from 0 up the helix and reading off where you end is the winding number — the encode map of the encode–decode proof.

DefinitionsH

Identity types, equivalences and univalence

Definition— identity type and path induction

For a type $A$ and $a : A$ , the identity type is a family of types $a =_A x$ indexed by $x : A$ , with one constructor $\mathsf{refl}_a : a =_A a$ . Its elimination rule is (based) path induction: given a family $C(x, p)$ for $x : A$ and $p : a = x$ , and an element $c : C(a, \mathsf{refl}_a)$ , there is a function $J(c) : \Pi_{x : A} \Pi_{p : a = x} C(x, p)$ with $J(c)(a, \mathsf{refl}_a) \equiv c$ . Elements of $a = x$ are called paths.

Path induction does not say that every $p : a = a$ is $\mathsf{refl}_a$ : the endpoint $x$ must be free. The rule that would say this, Streicher's axiom K (equivalently, uniqueness of identity proofs, UIP: any two elements of $a = b$ are equal), is independent of Martin-Löf type theory (Hofmann–Streicher) and false in homotopy type theory.

Definition— transport and the action on paths

From path induction one defines, for $p : a = b$ :

the inverse $p^{-1} : b = a$ and concatenation $p \cdot q : a = c$ for $q : b = c$ ;
the action of a function $f : A \to B$ on paths, $\mathsf{ap}_f(p) : f(a) = f(b)$ ;
transport in a family $P : A \to \mathcal{U}$ , a function $\mathsf{tr}^P(p, -) : P(a) \to P(b)$ .

Each is defined by saying what happens when $p$ is $\mathsf{refl}$ : $\mathsf{refl}^{-1} :\equiv \mathsf{refl}$ , $\mathsf{ap}_f(\mathsf{refl}) :\equiv \mathsf{refl}$ , $\mathsf{tr}^P(\mathsf{refl}, -) :\equiv \mathrm{id}$ .

Definition— contractible types, fibres and equivalences

A type $A$ is contractible if $\mathsf{isContr}(A) :\equiv \Sigma_{a : A} \Pi_{x : A} (a = x)$ is inhabited. The fibre of $f : A \to B$ over $b$ is $\mathsf{fib}_f(b) :\equiv \Sigma_{a : A} (f(a) = b)$ . A function is an equivalence if every fibre is contractible; equivalently (logically, though not as types), if it has a two-sided homotopy inverse $g$ with $\Pi_x\, g(f(x)) = x$ and $\Pi_y\, f(g(y)) = y$ . We write $A \simeq B$ for the type of equivalences. A type is a proposition if any two of its elements are equal, and a set if each of its identity types is a proposition.

Definition— univalence

Let $\mathcal{U}$ be a universe. By path induction there is a canonical map $\mathsf{idtoeqv} : (A =_{\mathcal{U}} B) \to (A \simeq B)$ sending $\mathsf{refl}_A$ to the identity equivalence. The univalence axiom (Voevodsky) states that $\mathsf{idtoeqv}$ is an equivalence for all $A, B : \mathcal{U}$ . Its inverse is written $\mathsf{ua} : (A \simeq B) \to (A = B)$ .

Definition— higher inductive types: the circle

A higher inductive type has constructors for paths as well as points. The circle $S^1$ has a point $\mathsf{base} : S^1$ and a path $\mathsf{loop} : \mathsf{base} = \mathsf{base}$ . Its recursion principle: to define $f : S^1 \to B$ it suffices to give $b : B$ and $\ell : b = b$ ; then $f(\mathsf{base}) \equiv b$ and $\mathsf{ap}_f(\mathsf{loop}) = \ell$ . Its induction principle does the same for dependent functions, with $\ell$ a path over $\mathsf{loop}$ : $\mathsf{tr}^P(\mathsf{loop}, b) = b$ .

Worked examplesH

Examples

Example— Transport in simple families

In a constant family $P(x) \equiv B$ , $\mathsf{tr}^P(p, -) = \mathrm{id}_B$ .
In the family $P(x) \equiv (a = x)$ of paths from a fixed point, $\mathsf{tr}^P(p, q) = q \cdot p$ : transporting a path along $p$ appends $p$ .
In the family $P(X) \equiv X$ over the universe, transport along $p : A = B$ is the underlying function of $\mathsf{idtoeqv}(p)$ , and univalence says that $\mathsf{tr}^{X \mapsto X}(\mathsf{ua}(e), -) = e$ .

Example— Sets, and a universe that is not a set

By Hedberg's theorem (1998), every type with decidable equality, such as $\mathbb{N}$ , $\Z$ or $\mathsf{Bool}$ , is a set. The universe is not: by univalence, $(\mathsf{Bool} = \mathsf{Bool}) \simeq (\mathsf{Bool} \simeq \mathsf{Bool})$ , and the right side has two different elements, the identity and negation. The path $\mathsf{ua}(\mathsf{not}) : \mathsf{Bool} = \mathsf{Bool}$ is a non-trivial loop in the universe — the universe "sees" the symmetry of $\mathsf{Bool}$ . More generally the type of $n$ -element types has loop space the symmetric group $S_n$ : it is the classifying space $BS_n$ .

Example— The circle is not a set

The loop $\mathsf{loop} : \mathsf{base} = \mathsf{base}$ is not equal to $\mathsf{refl}$ . The proof needs a type that is not a set: if every type were a set, the circle's recursion principle would send $\mathsf{loop}$ to $\mathsf{refl}$ in every type, but in the universe we can send it to $\mathsf{ua}(\mathsf{not})$ , which is not $\mathsf{refl}$ . The encode–decode theorem below computes $\mathsf{base} = \mathsf{base}$ completely.

ProofH

Central results

Theorem— Lemma 1 (the groupoid laws)

For paths $p : a = b$ , $q : b = c$ , $r : c = d$ : $\;\mathsf{refl} \cdot p = p$ , $\;p \cdot \mathsf{refl} = p$ , $\;p \cdot p^{-1} = \mathsf{refl}$ , $\;p^{-1} \cdot p = \mathsf{refl}$ and $(p \cdot q) \cdot r = p \cdot (q \cdot r)$ . These equalities are themselves paths, and they satisfy higher coherences (the pentagon and beyond).

Proof

Define $p \cdot q$ by induction on $q$ , setting $p \cdot \mathsf{refl} :\equiv p$ ; then the right unit law holds by definition. For the others, use path induction on the path with a free endpoint. For instance, to prove $\Pi_{x} \Pi_{p : a = x}\, (p \cdot p^{-1} = \mathsf{refl}_a)$ it suffices, by path induction, to treat $x \equiv a$ and $p \equiv \mathsf{refl}_a$ , where $\mathsf{refl} \cdot \mathsf{refl}^{-1} \equiv \mathsf{refl} \cdot \mathsf{refl} \equiv \mathsf{refl}$ , so $\mathsf{refl}_{\mathsf{refl}}$ is the required path. Associativity follows by induction on $r$ : both sides reduce to $p \cdot q$ . The left unit law $\mathsf{refl} \cdot p = p$ follows by induction on $p$ .

∎

Theorem— Lemma 2 (transport is an equivalence; transport is functorial)

For $P : A \to \mathcal{U}$ and $p : a = b$ , the function $\mathsf{tr}^P(p, -) : P(a) \to P(b)$ is an equivalence with inverse $\mathsf{tr}^P(p^{-1}, -)$ , and $\mathsf{tr}^P(p \cdot q, -) = \mathsf{tr}^P(q, -) \circ \mathsf{tr}^P(p, -)$ .

Proof

By path induction on $p$ (and on $q$ for the second claim): when $p \equiv \mathsf{refl}$ all transports are identities. A function with a two-sided inverse is an equivalence.

∎

Theorem— Theorem 3 (univalence contradicts uniqueness of identity proofs)

If the universe $\mathcal{U}$ is univalent and contains $\mathsf{Bool}$ , then $\mathcal{U}$ is not a set; in particular axiom K and UIP fail for $\mathcal{U}$ .

Proof

By univalence, $\mathsf{idtoeqv} : (\mathsf{Bool} = \mathsf{Bool}) \to (\mathsf{Bool} \simeq \mathsf{Bool})$ is an equivalence, in particular surjective. The identity equivalence and negation are different elements of $\mathsf{Bool} \simeq \mathsf{Bool}$ (they differ at $\mathsf{true}$ ). Their preimages $\mathsf{refl}$ and $\mathsf{ua}(\mathsf{not})$ are therefore different elements of $\mathsf{Bool} = \mathsf{Bool}$ , since $\mathsf{idtoeqv}$ sends them to different things. So $\mathsf{Bool} = \mathsf{Bool}$ is not a proposition, and $\mathcal{U}$ is not a set.

∎

The argument runs equally well backwards, and that is the content of the formal section: in a type theory where UIP holds — such as Lean, whose equality is proof-irrelevant — $\mathsf{idtoeqv}$ for $\mathsf{Bool}$ cannot be surjective, so univalence is false, not merely unprovable.

Theorem— Theorem 4 (univalence implies function extensionality; Voevodsky; stated)

In a univalent universe, if $f, g : \Pi_{x : A} B(x)$ satisfy $\Pi_x\, f(x) = g(x)$ , then $f = g$ . Moreover the canonical map $(f = g) \to \Pi_x (f(x) = g(x))$ is an equivalence.

See Homotopy Type Theory, §4.9. Function extensionality is not provable in plain Martin-Löf type theory; in HoTT it is a consequence of univalence, while in Lean it is a theorem derived from quotient types.

Theorem— Theorem 5 (the loop space of the circle; Licata and Shulman, 2013)

$(\mathsf{base} =_{S^1} \mathsf{base}) \simeq \Z$ . Consequently $\pi_1(S^1) \cong \Z$ , and $S^1$ is a 1-type (its higher homotopy groups vanish).

Proof

(Outline of the encode–decode method.)

The universal cover. Define $\mathsf{code} : S^1 \to \mathcal{U}$ by circle recursion, with $\mathsf{code}(\mathsf{base}) :\equiv \Z$ and $\mathsf{ap}_{\mathsf{code}}(\mathsf{loop}) := \mathsf{ua}(\mathsf{succ})$ , where $\mathsf{succ} : \Z \simeq \Z$ is the successor. By the computation rules of circle recursion and univalence, $\mathsf{tr}^{\mathsf{code}}(\mathsf{loop}, n) = n + 1$ and $\mathsf{tr}^{\mathsf{code}}(\mathsf{loop}^{-1}, n) = n - 1$ .
Encode. For $x : S^1$ define $\mathsf{encode} : (\mathsf{base} = x) \to \mathsf{code}(x)$ by $\mathsf{encode}(p) :\equiv \mathsf{tr}^{\mathsf{code}}(p, 0)$ .
Decode. Define $\mathsf{decode} : \Pi_{x : S^1}\, \mathsf{code}(x) \to (\mathsf{base} = x)$ by circle induction: $\mathsf{decode}(\mathsf{base}, n) :\equiv \mathsf{loop}^n$ , and one checks that this is compatible with transport along $\mathsf{loop}$ , which amounts to $\mathsf{loop}^{n-1} \cdot \mathsf{loop} = \mathsf{loop}^n$ .
Decode after encode. $\mathsf{decode}(x, \mathsf{encode}(p)) = p$ for all $x$ and $p : \mathsf{base} = x$ , by based path induction on $p$ : for $p \equiv \mathsf{refl}$ both sides are $\mathsf{refl}$ , since $\mathsf{encode}(\mathsf{refl}) \equiv 0$ and $\mathsf{loop}^0 \equiv \mathsf{refl}$ .
Encode after decode. $\mathsf{encode}(\mathsf{decode}(x, c)) = c$ , by circle induction reduced to $x \equiv \mathsf{base}$ , where it says $\mathsf{tr}^{\mathsf{code}}(\mathsf{loop}^n, 0) = n$ . By functoriality of transport (Lemma 2) this is $\mathsf{succ}^n(0) = n$ , an induction on $n \in \Z$ .

So $(\mathsf{base} = x) \simeq \mathsf{code}(x)$ for all $x$ , and at $x \equiv \mathsf{base}$ this gives $(\mathsf{base} = \mathsf{base}) \simeq \Z$ . Since $\Z$ is a set, the loop space is a set, so $\pi_1(S^1) \cong \Z$ and $S^1$ has no higher homotopy. Full details: Homotopy Type Theory, §8.1, and Licata–Shulman (2013).

∎

Step 1 is where univalence enters, and step 3 is where the higher inductive type does. The formal section proves the purely arithmetic step 5 (that $\mathsf{succ}^n(0) = n$ for every integer $n$ ) in Lean, and cites Mathlib's classical proof that $\pi_1(S^1) \cong \Z$ via covering spaces.

Theorem— Theorem 6 (models; stated)

Univalent type theory has a model in Kan simplicial sets, in which types are Kan complexes and identity types are path spaces (Voevodsky; Kapulkin and Lumsdaine, 2021); the model also interprets many higher inductive types, including the circle (Lumsdaine and Shulman, 2020). This shows that univalence is consistent relative to ZFC with inaccessible cardinals (used to interpret universes).
Cubical type theory has constructive models in cubical sets, in which univalence is a theorem and computes (Bezem, Coquand and Huber, 2014; Cohen, Coquand, Huber and Mörtberg, 2018).
Every Grothendieck $(\infty, 1)$ -topos models homotopy type theory with strict univalent universes (Shulman, 2019).

ExplanationH

The landscape: what is known and what is open

Established.

Synthetic homotopy theory. Classical theorems have been reproved inside HoTT, where they hold in every model: $\pi_1(S^1) = \Z$ , $\pi_k(S^n) = 0$ for $k < n$ , $\pi_n(S^n) = \Z$ , the Hopf fibration and $\pi_3(S^2) = \Z$ , the Freudenthal suspension theorem, Eilenberg–MacLane spaces (Licata–Finster, 2014), and the Blakers–Massey theorem (Favonia, Finster, Licata and Lumsdaine, 2016). Brunerie (2016) proved that $\pi_4(S^3) \cong \Z/n$ for an explicitly defined integer $n$ and then showed by hand that $n = \pm 2$ ; getting a proof assistant to compute $n$ was an open challenge for years, met with a reformulated proof in Cubical Agda (Ljungström and Mörtberg, 2023).
Univalent mathematics. Large libraries (UniMath, the Coq HoTT library, agda-unimath) develop algebra and category theory univalently. Univalent categories satisfy "isomorphic objects are equal", and every category has a univalent completion, the Rezk completion (Ahrens, Kapulkin and Shulman, 2015).
Logic. The law of excluded middle for propositions and the axiom of choice for sets are consistent with univalence (they hold in the simplicial model), but excluded middle for all types, $\Pi_{A : \mathcal{U}} (A + \neg A)$ , contradicts univalence (HoTT, §3.2).

Open or in progress.

Which further homotopy groups of spheres can be computed synthetically, and how efficiently proofs about them can be made to compute.
The precise sense in which HoTT is the internal language of $(\infty, 1)$ -toposes: partial results exist (for example Kapulkin and Szumiło, 2019, for finitely complete $(\infty, 1)$ -categories), but a full statement covering univalent universes and higher inductive types is not established.
Synthetic ∞-category theory in directed or simplicial type theories (Riehl and Shulman, 2017) and new type theories that make univalence and higher inductive types compute in every model are active research programmes.

Formal mathematicsF

HoTT and Lean: where they part ways

Lean's logic is a dependent type theory, but not homotopy type theory: its equality a = b lives in the universe Prop of proof-irrelevant propositions, so any two proofs of a = b are equal by definition. This is uniqueness of identity proofs, which, by Theorem 3, contradicts univalence. We can still learn a lot by building a HoTT-style identity type inside Lean and watching what happens.

First, an identity type in Type rather than Prop, with its eliminator. J is defined by pattern matching on refl with the endpoint free, which is exactly based path induction:

PathsLean 4Formally verified

/-- The **identity type** of `A`, based at `a`: an inductive family `Paths a b` with a single
constructor `refl : Paths a a`. Read an element `p : Paths a b` as a *path* from `a` to `b`.
Unlike Lean's `Eq`, which lives in `Prop`, this type lives in `Type u`, so its elements are data
and can, a priori, be distinct. -/
inductive Paths {A : Type u} (a : A) : A → Type u
  | refl : Paths a a

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

JLean 4Formally verified

/-- **Path induction** (the `J` eliminator, in Paulin-Mohring's based form). To construct an
element of `C b p` for *every* `b` and every path `p : Paths a b`, it suffices to construct one
for `b = a` and `p = refl`. Pattern matching on `refl` with the endpoint `b` free is exactly
this rule; everything below is built from `J` alone. -/
def J {A : Type u} {a : A} (C : (b : A) → Paths a b → Sort v) (c : C a refl) :
    {b : A} → (p : Paths a b) → C b p
  | _, refl => c

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

The basic operations, each defined from J alone, exactly as in the definitions section:

invLean 4Formally verified

/-- The inverse of a path, by path induction: the inverse of `refl` is `refl`. -/
def inv {A : Type u} {a b : A} (p : Paths a b) : Paths b a :=
  J (fun b _ => Paths b a) refl p

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

concatLean 4Formally verified

/-- Concatenation of paths, by path induction on the second path: `p ⬝ refl = p`. -/
def concat {A : Type u} {a b c : A} (p : Paths a b) (q : Paths b c) : Paths a c :=
  J (fun c _ => Paths a c) p q

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

apLean 4Formally verified

/-- **Functions act on paths**: `ap f : Paths a b → Paths (f a) (f b)`. Every function is
automatically "continuous" in HoTT, because it must respect path induction. -/
def ap {A : Type u} {B : Type v} (f : A → B) {a b : A} (p : Paths a b) : Paths (f a) (f b) :=
  J (fun b _ => Paths (f a) (f b)) refl p

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

transportLean 4Formally verified

/-- **Transport**: a path `p : Paths a b` in the base gives a function `P a → P b` between the
fibres of any type family `P`. Geometrically: lifting a path to a fibration. Logically: the
indiscernibility of identicals (Leibniz's law). -/
def transport {A : Type u} (P : A → Type v) {a b : A} (p : Paths a b) : P a → P b :=
  J (fun b _ => P a → P b) id p

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

The groupoid laws and functoriality of transport (Lemmas 1 and 2), proved by path induction. Because a proof of an equation between paths is itself a path — an element of a type in Type — these are defs producing paths, not theorems: Lean reserves theorem for propositions.

refl_concatLean 4Proved here from basic factsFormally verified

/-- Left unit law, `refl ⬝ p = p`, as a **path** between paths, constructed by path induction on
`p`. (The right unit law `p ⬝ refl = p` holds by definition of `concat`.) In HoTT a proof of an
equation is an element of an identity type, so this is a `def`: Lean reserves `theorem` for
statements in `Prop`, and `Paths` lives in `Type`. -/
def refl_concat {A : Type u} {a b : A} (p : Paths a b) : Paths (concat refl p) p :=
  J (fun _ p => Paths (concat refl p) p) refl p

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

concat_invLean 4Proved here from basic factsFormally verified

/-- Inverse law: `p ⬝ p⁻¹ = refl`, as a path, by path induction on `p`. -/
def concat_inv {A : Type u} {a b : A} (p : Paths a b) : Paths (concat p (inv p)) refl :=
  J (fun _ p => Paths (concat p (inv p)) refl) refl p

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

concat_assocLean 4Proved here from basic factsFormally verified

/-- Associativity: `(p ⬝ q) ⬝ r = p ⬝ (q ⬝ r)`, as a path, by path induction on `r` (both sides
then reduce to `p ⬝ q`). In HoTT these laws are themselves paths, and they satisfy further
laws (the pentagon, …) up to higher paths: every type is a weak ∞-groupoid. -/
def concat_assoc {A : Type u} {a b c d : A} (p : Paths a b) (q : Paths b c) (r : Paths c d) :
    Paths (concat (concat p q) r) (concat p (concat q r)) :=
  J (fun _ r => Paths (concat (concat p q) r) (concat p (concat q r))) refl r

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

transport_concatLean 4Proved here from basic factsFormally verified

/-- Transport is functorial: transporting along `p ⬝ q` is transporting along `p` and then along
`q`. (A path, by induction on `q`.) This is what makes `transport` into a functor from the
path groupoid of `A` to types. -/
def transport_concat {A : Type u} (P : A → Type v) {a b c : A} (p : Paths a b)
    (q : Paths b c) (x : P a) :
    Paths (transport P (concat p q) x) (transport P q (transport P p x)) :=
  J (fun _ q => Paths (transport P (concat p q) x) (transport P q (transport P p x))) refl q

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

The map that univalence asks to be an equivalence:

idtoeqvLean 4Formally verified

/-- The canonical map from paths between types to equivalences, `idtoeqv`: by path induction it
sends `refl` to the identity equivalence. **Voevodsky's univalence axiom** says that this map is
itself an equivalence, for all types `A` and `B` in a universe. -/
def idtoeqv {A B : Type u} (p : Paths A B) : A ≃ B :=
  J (fun B _ => A ≃ B) (Equiv.refl A) p

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

Now the two theorems about Lean itself. Even though Paths a b lives in Type, Lean proves it has at most one element: it is a retract of a = b, which is proof-irrelevant. The middle step of the calc is closed by rfl, because Lean considers any two proofs of the same proposition definitionally equal. Consequently idtoeqv is not surjective for Bool, and univalence is false in Lean:

paths_subsingletonLean 4Proved here from basic factsFormally verified

/-- **Uniqueness of identity proofs holds in Lean**, even for our `Type`-valued `Paths`: any two
paths `p q : Paths a b` are equal. Proof: `Paths a b` is a *retract* of Lean's `a = b` (map a path
to an equality, and back, and path induction shows the round trip is the identity), and `a = b`
is a proposition with at most one proof (Lean has definitional proof irrelevance). A retract of
a type with at most one element has at most one element. In HoTT this fails: the type of paths
from a point to itself in the circle is `ℤ`. -/
theorem paths_subsingleton {A : Type u} {a b : A} (p q : Paths a b) : p = q := by
  -- From paths to Lean equalities, and back.
  let toEq : {b : A} → Paths a b → a = b := fun p => J (fun b _ => a = b) rfl p
  let ofEq : {b : A} → a = b → Paths a b := fun h => h ▸ refl
  -- The round trip is the identity (path induction, with a motive in `Prop`).
  have round : ∀ {b : A} (p : Paths a b), ofEq (toEq p) = p := by
    intro b p
    exact J (fun _ p => ofEq (toEq p) = p) rfl p
  -- `toEq p` and `toEq q` are proofs of the same proposition, hence equal.
  calc p = ofEq (toEq p) := (round p).symm
    _ = ofEq (toEq q) := rfl
    _ = q := round q

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

univalence_failsLean 4Proved here from basic factsFormally verified

/-- **The univalence axiom is false in Lean.** The map `idtoeqv : Paths Bool Bool → (Bool ≃ Bool)`
is not surjective: there are two equivalences `Bool ≃ Bool` (the identity and negation), but at
most one path `Bool = Bool` (`paths_subsingleton`). So univalence cannot be added to Lean as an
axiom without making Lean inconsistent; HoTT needs a type theory *without* uniqueness of identity
proofs. -/
theorem univalence_fails : ¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool)) := by
  intro hsurj
  obtain ⟨p, hp⟩ := hsurj (Equiv.refl Bool)
  obtain ⟨q, hq⟩ := hsurj Equiv.boolNot
  -- `p = q`, so the identity and negation would be the same equivalence.
  have hpq : p = q := paths_subsingleton p q
  have h : Equiv.refl Bool = Equiv.boolNot := by rw [← hp, ← hq, hpq]
  -- Evaluate both at `true`.
  have h' : true = false := congrArg (fun e : Bool ≃ Bool => e true) h
  exact Bool.noConfusion h'

Axioms used: Quot.soundformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

Function extensionality, which HoTT derives from univalence, is a theorem in Lean derived from quotient types; and the set-level shadow of "equivalences are maps with contractible fibres" is Mathlib's characterisation of bijections:

funext_libraryLean 4Applies a library theoremFormally verified

/-- **Function extensionality**: pointwise equal functions are equal. In HoTT it is a theorem
deduced from univalence (Voevodsky); in Lean it is a theorem deduced from quotient types
(`Quot.sound`). This applies core Lean's `funext`. -/
theorem funext_library {α : Type u} {β : α → Type v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g :=
  funext h

Axioms used: Quot.soundformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

bijective_iff_unique_fibresLean 4Applies a library theoremFormally verified

/-- The set-level shadow of "an equivalence is a map with contractible fibres": a function is
bijective exactly when every fibre `{a | f a = b}` has exactly one element. (In HoTT,
"contractible" replaces "has exactly one element", and the definition then works for types with
higher paths too.) This applies Mathlib's `Function.bijective_iff_existsUnique`. -/
theorem bijective_iff_unique_fibres {α : Type u} {β : Type v} (f : α → β) :
    Function.Bijective f ↔ ∀ b, ∃! a, f a = b :=
  Function.bijective_iff_existsUnique f

Axioms used: No axiomsformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

Finally, the circle. Lean has no higher inductive types, but Mathlib proves the classical theorem $\pi_1(S^1) \cong \Z$ with covering spaces, and we prove the arithmetic step 5 of the encode–decode argument — the $n$ -th power of the successor permutation of $\Z$ is translation by $n$ , for negative $n$ too:

fundamental_group_circleLean 4Applies a library theoremFormally verified

/-- **The classical theorem: `π₁(S¹) ≅ ℤ`.** Mathlib's `AddCircle.windingNumberIso` proves it
for the circle `ℝ / pℤ` using covering-space theory (the universal cover `ℝ → S¹`), sending a
loop to its winding number. Homotopy type theory proves a synthetic version, `Ω(S¹) ≃ ℤ`, for
the higher inductive circle (Licata and Shulman, 2013). -/
theorem fundamental_group_circle (p : ℝ) [Fact (0 < p)] (x : AddCircle p) :
    Nonempty (FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ) :=
  ⟨AddCircle.windingNumberIso x⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

encode_loop_powLean 4Proved here from basic factsFormally verified

/-- **The arithmetic step of encode–decode.** In the HoTT proof, the universal cover of the
circle is the family `code : S¹ → U` with `code(base) = ℤ`, and univalence makes transport along
`loop` equal to the successor `succ : ℤ ≃ ℤ`. Since transport turns concatenation into
composition (`transport_concat`), transport along `loopⁿ` is `succⁿ`, and `encode(loopⁿ)` is
`succⁿ(0)`. Here we prove the last step in ordinary Lean: the `n`-th power of the successor
permutation of `ℤ` sends `k` to `k + n`, for every integer `n` (negative powers included). In
particular `succⁿ(0) = n`. -/
theorem encode_loop_pow (n k : ℤ) : ((Equiv.addRight (1 : ℤ)) ^ n) k = k + n := by
  induction n using Int.induction_on generalizing k with
  | zero => simp
  | succ m ih =>
    rw [zpow_add_one, Equiv.Perm.mul_apply, ih]
    simp only [Equiv.coe_addRight]
    ring
  | pred m ih =>
    rw [zpow_sub_one, Equiv.Perm.mul_apply, ih]
    simp only [Equiv.Perm.inv_def, Equiv.addRight_symm, Equiv.coe_addRight]
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HomotopyTypeTheory.leanTry it in the Lean web editor

What is and is not formalised. Formalised here: identity types with path induction, the groupoid laws and transport as paths, the map idtoeqv, and two precise theorems showing that Lean validates uniqueness of identity proofs and refutes univalence. Not formalisable in Lean as it stands: univalent universes, higher inductive types, and the synthetic proof of Theorem 5. Those live in proof assistants built for HoTT — Cubical Agda, Coq/Rocq with the HoTT library, UniMath, Arend — in which, conversely, Lean's proof-irrelevant Prop is unavailable.

ComputationC

Encode and decode, by machine

In a combinatorial model of the circle, a loop built from $\mathsf{loop}$ and $\mathsf{loop}^{-1}$ is a word in $+1$ and $-1$ , the groupoid laws cancel adjacent $+1, -1$ , and transport in the universal cover is successor and predecessor on $\Z$ . The experiment checks exhaustively, for all 8190 non-empty words of length at most 12, that decoding the winding number gives back the reduced word (steps 4 and 5 of Theorem 5 in this model), that encoding turns concatenation into addition, and then computes winding numbers of loops in the plane numerically, the classical counterpart.

Encode-decode for the circle: words, winding numbers, ZPythonExact computationExhaustive finite checkNumerical approximationComputationally tested

"""Encode-decode for the circle, in a combinatorial model, and winding numbers.

In homotopy type theory the circle S^1 has a point base and a path loop. Loops
at base built from loop and its inverse are modelled here by words in +1
(loop) and -1 (loop inverse); concatenation of paths is concatenation of
words, and the groupoid laws p . p^-1 = refl let us cancel adjacent +1, -1.
The universal cover is the type family code with code(base) = Z, where
transport along loop is the successor. So:

* encode(w) = transport of 0 along w = apply succ for +1 and pred for -1;
* decode(n) = loop^n, the word of |n| copies of the sign of n.

We check exhaustively, for all words of length <= 12, that decode(encode(w))
is the free reduction of w (so two words are equal up to the groupoid laws
exactly when they have the same winding number) and that encode turns
concatenation into addition; then compute winding numbers of parametrised
loops in the plane numerically, the classical counterpart. This is a model and
finite evidence, not the HoTT proof, which is about the higher inductive type.
"""

import cmath
import math
from itertools import product

def encode(word):
    """Transport 0 along the path ``word`` in the universal cover of S^1.

    Transport along loop is succ, along its inverse pred; transport along a
    concatenation is the composite of the transports.
    """
    position = 0
    for step in word:
        if step not in (1, -1):
            raise ValueError("a word consists of +1 (loop) and -1 (loop^-1)")
        position = position + 1 if step == 1 else position - 1
    return position

def decode(n):
    """The loop loop^n as a word: |n| copies of +1 (n > 0) or -1 (n < 0)."""
    return (1,) * n if n >= 0 else (-1,) * (-n)

def reduce_word(word):
    """Free reduction: cancel adjacent loop . loop^-1 and loop^-1 . loop."""
    stack = []
    for step in word:
        if stack and stack[-1] == -step:
            stack.pop()
        else:
            stack.append(step)
    return tuple(stack)

def inverse(word):
    """The inverse path: reverse the word and invert each letter."""
    return tuple(-s for s in reversed(word))

def all_words(max_length):
    """Every word of length 1..max_length in the letters +1 and -1."""
    for length in range(1, max_length + 1):
        yield from product((1, -1), repeat=length)

def winding_number(curve, samples=2000):
    """Numerical winding number of a closed curve t -> curve(t) around 0,
    t in [0, 1], by summing the changes of argument between samples."""
    total = 0.0
    previous = curve(0.0)
    for i in range(1, samples + 1):
        current = curve(i / samples)
        total += cmath.phase(current / previous)
        previous = current
    return total / (2 * math.pi)

def wobbly_loop(turns, wobble=0.6, frequency=7):
    """A loop that winds ``turns`` times round 0 with a radial wobble."""
    def curve(t):
        radius = 1 + wobble * math.cos(2 * math.pi * frequency * t)
        return radius * cmath.exp(2j * math.pi * turns * t)
    return curve

def main():
    words = list(all_words(12))
    decoded_ok = all(decode(encode(w)) == reduce_word(w) for w in words)
    print(f"Words of length 1..12: {len(words)}")
    print(f"decode(encode(w)) == reduce(w) for every word: {decoded_ok}")
    print("encode(decode(n)) == n for -50 <= n <= 50:",
          all(encode(decode(n)) == n for n in range(-50, 51)))
    short = list(all_words(6))
    additive = all(encode(u + v) == encode(u) + encode(v)
                   for u in short for v in short)
    print(f"encode(u . v) == encode(u) + encode(v) for words up to 6: "
          f"{additive}")
    print("encode(w^-1) == -encode(w) for all words up to 12:",
          all(encode(inverse(w)) == -encode(w) for w in words))
    null = [w for w in product((1, -1), repeat=10) if encode(w) == 0]
    print(f"Words of length 10 with winding number 0: {len(null)} "
          f"(= C(10,5) = {math.comb(10, 5)});")
    print("   all of them reduce to refl:",
          all(reduce_word(w) == () for w in null))
    print()
    print("Classical counterpart: winding numbers of plane loops (numerical)")
    for turns in (1, 3, -2, 0):
        w = winding_number(wobbly_loop(turns))
        print(f"   loop winding {turns:>2} times with a wobble: "
              f"computed {w:+.6f}, |error| < 1e-9: {abs(w - turns) < 1e-9}")
    print()
    print("Epistemic status: exact, exhaustive checks of a combinatorial model")
    print("(words up to length 12), plus floating-point winding numbers. They")
    print("illustrate the encode-decode equivalence of loops with Z but do not")
    print("prove the HoTT theorem, which concerns the higher inductive circle.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Explore

Explore: transport along a path

Transport and the action of functions on paths fit into one picture. A path $p$ in the base type $A$ lifts to the total space of a family $P$ ; over the circle with the family $\mathsf{code}$ , lifting $\mathsf{loop}$ starting at $0$ ends at $1$ .

Top: transport along a path

p : a = b

(drawn as a double arrow) is a function between fibres, an equivalence by Lemma 2. Bottom: in the universal cover of the circle, transport along

\mathsf{loop}

is the successor; the experiment's encode map iterates it along a word.

Try it with the experiment's functions in mind: the word $(+1, +1, -1, +1)$ encodes to $2$ because transport along a concatenation is the composite of transports. Which words of length 4 encode to $0$ , and why do all of them reduce to the empty word?

Exercises

1. Homotopy type theory

Warm-upHuman

In the homotopy interpretation, what is the identity type $a =_A b$ ?

Choose one

The space of paths in

A

from

a

b

A truth value: true if

a

and

b

are equal, false otherwiseThe set

\{a, b\}

The set of isomorphisms between

a

and

b

, by definition

2. Homotopy type theory

Warm-upHuman

Assume univalence. How many elements does the identity type $\mathsf{Fin}(3) = \mathsf{Fin}(3)$ have (it is a set, so count elements up to paths)?

3. Homotopy type theory

CoreHuman

Let $P(x) :\equiv (a = x)$ for a fixed $a : A$ . For $p : b = c$ and $q : a = b$ , what is $\mathsf{tr}^P(p, q) : a = c$ ?

Choose one

q \cdot p

p \cdot q

q

, since transport is just substitution

p^{-1} \cdot q

4. Homotopy type theory

CoreHuman

A student argues: 'Let $p : a = a$ . By path induction we may assume $p$ is $\mathsf{refl}_a$ , so every loop equals $\mathsf{refl}_a$ .' What is wrong?

Choose one

Path induction applies only to families over paths with a free endpoint,

\Pi_{x}\Pi_{p : a = x} C(x, p)

; here both endpoints are fixed at

a

Nothing: this is a valid proof of uniqueness of identity proofsThe argument forgot to use symmetry of equalityPath induction requires function extensionality

5. Homotopy type theory

CoreFormal

Which Lean statement expresses that univalence fails in Lean, for the type Bool?

Choose one

¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool))¬ Nonempty (Paths Bool Bool)Function.Injective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool))¬ (Bool ≃ Bool)

6. Homotopy type theory

CoreHuman

In the encode–decode proof that $(\mathsf{base} = \mathsf{base}) \simeq \Z$ , where is the univalence axiom used?

Choose one

To define the universal cover

\mathsf{code}

, sending

\mathsf{loop}

to the path

\mathsf{ua}(\mathsf{succ}) : \Z = \Z

in the universeTo prove

\mathsf{decode}(\mathsf{encode}(p)) = p

To prove

\mathsf{succ}^n(0) = n

by induction on

n

Nowhere; the higher inductive circle suffices

7. Homotopy type theory

CoreHuman

Which principles are consistent with (or follow from) univalence? (Choose all that apply.)

Choose all that apply

Excluded middle for propositionsThe axiom of choice for setsFunction extensionalityUniqueness of identity proofs for all types, including the universeExcluded middle for all types,

\Pi_{A : \mathcal{U}} (A + \neg A)

8. Homotopy type theory

StretchHuman

In homotopy type theory with univalence and the higher inductive circle, which of these types are sets (all of their identity types are propositions)? (Choose all that apply.)

Choose all that apply

9. Homotopy type theory

StretchComputational

Loops in the circle built from $\mathsf{loop}$ ( $+1$ ) and $\mathsf{loop}^{-1}$ ( $-1$ ) are words, e.g. (1, 1, -1). The groupoid laws let us cancel an adjacent pair 1, -1 or -1, 1. Write reduce_word(word) returning the fully reduced word as a tuple. (The tests check that your reduced word is always $\mathsf{decode}(\mathsf{encode}(w))$ .)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"HoTT replaces set theory and category theory wholesale." It is one foundation among several, with its own strengths (invariance under equivalence is built in; homotopy theory becomes synthetic) and open questions (computation with univalence in all models, the precise relation to ∞-toposes). Much mathematics can be done in ZFC, in Lean's type theory or in HoTT, and the interpretations between them are themselves mathematics.

Misconception

"Univalence says isomorphic sets are equal, so it contradicts ZFC." Univalence is an axiom about identity types inside type theory; it says nothing about membership of ZFC sets. It is consistent relative to ZFC with inaccessible cardinals, via the simplicial-set model, in which " $A = B$ " is interpreted as a space of paths, not as equality of sets.

Misconception

"HoTT is the same as ∞-category theory." They are connected through models: types in a model behave like objects of an ∞-topos (Shulman), and ∞-groupoids appear on both sides. But HoTT is a formal language with proofs and computation, and directed ∞-categories (with non-invertible morphisms) are not what its identity types describe.

Misconception

"Path induction says every path is refl." Path induction lets you assume $p \equiv \mathsf{refl}$ only when one endpoint is free. For a loop $p : a = a$ with both endpoints fixed, the rule does not apply — which is why $\mathsf{loop} \neq \mathsf{refl}$ in the circle and $\mathsf{ua}(\mathsf{not}) \neq \mathsf{refl}$ in the universe.

Misconception

"Lean can check HoTT proofs if we are careful." Lean's equality satisfies uniqueness of identity proofs definitionally, and so Lean refutes univalence (formal section). One can study HoTT about Lean-built models, or restrict oneself to a fragment, but univalent proofs need a proof assistant designed without proof-irrelevant equality.

ViewpointsH

Many ways of seeing

Topology— Synthetic homotopy theory

To a topologist, HoTT is a language in which every type is a space and every construction is automatically continuous: a function $f : A \to B$ acts on paths ( $\mathsf{ap}_f$ ), a type family is a fibration (transport is path lifting), and $\Sigma$ and $\Pi$ are total spaces and spaces of sections. Spaces are described synthetically, by generators (higher inductive types), rather than as sets of points with a topology. Theorem 5 is the type-theoretic version of the covering-space proof that $\pi_1(S^1) \cong \Z$ , with $\mathsf{code}$ playing the universal cover $\R \to S^1$ — and because it uses only the rules of type theory, it holds in every ∞-topos. See Homotopy and the fundamental group.

Logic— Propositions as some types

Curry–Howard reads every type as a proposition; HoTT refines this. Only types with at most one element (up to paths) are propositions in the HoTT sense, and the propositional truncation $\|A\|$ turns any type into one ("there merely exists"). This resolves an old tension: $\Sigma_{x : A} P(x)$ remembers a witness, while $\|\Sigma_{x : A} P(x)\|$ is the classical "there exists". Excluded middle and choice can be assumed for propositions and sets without contradicting univalence, but excluded middle for all types contradicts it, because it would choose, uniformly in $A$ , an element of every inhabited type — impossible when the universe has symmetries. See Proof theory and Categorical logic.

Algebra— Groups as pointed connected types

In univalent foundations a group can be presented as a pointed, connected 1-type $BG$ , with $G$ recovered as the loop space $\mathsf{pt} = \mathsf{pt}$ : composition is concatenation and associativity is Lemma 1. Actions of $G$ on sets are type families over $BG$ , homomorphisms are pointed maps $BG \to BH$ , and the circle is $B\Z$ (Theorem 5). The universe itself realises symmetric groups: the type of $n$ -element types is $BS_n$ . This approach to group theory is developed in the draft book Symmetry by Bezem, Buchholtz, Cagne, Dundas and Grayson. See Groups.

Combinatorics— Counting symmetries: groupoid cardinality

Univalence says that the paths $\mathsf{Fin}(n) = \mathsf{Fin}(n)$ are the $n!$ permutations. Counting a groupoid by weighting each isomorphism class by $1/|\mathrm{Aut}|$ (Baez and Dolan, 2001), the type of all finite sets has cardinality $\sum_{n \ge 0} 1/n! = e$ . This "homotopy cardinality" is the bookkeeping behind exponential generating functions and Joyal's combinatorial species, where structures on finite sets are counted up to relabelling — exactly the invariance under equivalence that univalence builds in. See Enumerative combinatorics.

Computation— Proofs that compute

In type theory, proofs are programs, and closed terms should compute to canonical values. An axiom such as univalence blocks computation: a term of type $\mathbb{N}$ built using $\mathsf{ua}$ may not reduce to a numeral. Cubical type theory solves this by taking paths to be maps out of an abstract interval, so that univalence becomes a theorem that computes; Huber (2019) proved canonicity for cubical type theory. Cubical Agda implements it, and the computation of Brunerie's number (Ljungström and Mörtberg) is a striking test of what "proofs that compute" can achieve. See Formal methods.

Category theory— ∞-toposes and univalent categories

Categorically, a model of HoTT is a type-theoretic model topos, presenting an $(\infty, 1)$ -topos, in which types are objects, dependent types are fibrations and univalent universes are object classifiers (Shulman, 2019). Inside HoTT, category theory itself becomes univalent: a univalent category is one in which the canonical map from identities of objects to isomorphisms is an equivalence — so "isomorphic objects are equal" holds by design, and constructions automatically respect isomorphism. See ∞-categories and Elementary topos theory.

History & global context

History and global context

1970s–1980s. Per Martin-Löf (Stockholm) developed intensional dependent type theory, with identity types and their elimination rule $J$ ; Thierry Coquand and Gérard Huet's calculus of constructions (1988) led to the proof assistants Coq (now Rocq) and, later, Lean.
1990s: identity proofs need not be unique. Martin Hofmann and Thomas Streicher (Germany) built the groupoid model (1994), showing that uniqueness of identity proofs is not provable; Streicher formulated axiom K; Hedberg (1998) showed that types with decidable equality satisfy UIP.
2006–2010: the homotopy interpretation. Steve Awodey and Michael Warren showed that identity types can be interpreted as path objects in model categories; Vladimir Voevodsky, independently, built the simplicial model and formulated univalence and univalent foundations, motivated in part by errors discovered in published proofs, including his own (see Higher categories); Lumsdaine and van den Berg–Garner showed that types are weak ∞-groupoids.
2012–2013: the special year. A special year at the Institute for Advanced Study in Princeton brought together researchers from many countries and produced the collaboratively written Homotopy Type Theory book (2013). Licata and Shulman computed the loop space of the circle (2013).
2014–today. Cubical type theory (Bezem, Coquand, Huber; Cohen, Coquand, Huber, Mörtberg) gave univalence computational meaning; Shulman (2019) showed that all ∞-toposes model HoTT; large univalent libraries and textbooks (Rijke, 2022) appeared; Brunerie's computation of $\pi_4(S^3)$ and its mechanisation became landmarks of synthetic homotopy theory.

What does it mean to be the same?

A dictionary

Identity types, equivalences and univalence

Examples

Central results

The landscape: what is known and what is open

HoTT and Lean: where they part ways

Encode and decode, by machine

Explore: transport along a path

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading