Homotopy Type Theory (HoTT)

What if mathematics were founded not on sets but on spaces? What if equality were a path, and a proof were a program? Homotopy type theory answers: yes, this is possible - and it is better. HoTT is one of the most radical ideas in mathematics in recent decades, born at the crossroads of topology, logic, and the theory of computation.

• **Formal verification:** The UniMath project (Voevodsky) and Mathlib4 (Lean) use HoTT principles to machine-verify hundreds of theorems in algebraic topology and algebra
• **Programming languages:** Dependent types (Agda, Idris, Lean) are the practical realization of HoTT ideas; type-safe programs with formal guarantees
• **Artificial intelligence:** Neurosymbolic systems use type theory for formal reasoning; HoTT-inspired architectures handle symmetries as equivalences

Предварительные знания

• Topological Quantum Computing

Types as Topological Spaces

In **homotopy type theory** (HoTT) a type A is interpreted as a topological space, its elements a: A as points, and proofs of equality p: a = b as **paths** between points. This is a revolutionary perspective: logic and topology are the same thing.

The type S¹ in HoTT is defined inductively: one base point base: S¹ and one path loop: base = base. This is precisely the description of a circle! One can then compute: π₁(S¹) = Z - via induction on the type S¹ and the recursion principle. This is one of the first non-trivial topological computations carried out entirely inside type theory.

Voevodsky's Univalence Axiom

The **univalence axiom** (Voevodsky, 2010) states: A ≃ B ↔ A = B. Equivalence of types equals their identity. This formalizes the mathematical principle that 'isomorphic objects are interchangeable' and has deep consequences for the foundations of mathematics.

The univalence axiom is revolutionary: in classical set theory, isomorphic structures can be 'different sets'. In HoTT, isomorphism = identity. This formalizes how mathematicians actually think: the group Z/2 and {±1} are 'the same thing', even though formally they are different sets.

Inductive Types and Their Homotopical Meaning

**Inductive types** are types defined by constructors and a recursion principle. In HoTT they describe both ordinary data structures (natural numbers, lists) and topological spaces (S¹, torus, suspensions).

Higher inductive types (HITs) allow defining arbitrary CW complexes inside type theory: base constructors = 0-cells, path constructors = 1-cells, homotopy constructors = 2-cells. This merges synthetic topology with dependent types: topological invariants of types can be 'computed' as programs in Lean 4 or Agda.

HoTT as a Foundation of Mathematics

Voevodsky's program: **univalent foundations of mathematics**: using HoTT as an alternative to set theory ZFC. Mathematical objects are types, proofs are programs, theorems are machine-verified. ∞-groupoids are the right 'manifolds' in this world.

In ZFC, 'equality' is rigid: two objects are equal or they are not. In HoTT, equality is a space of paths with rich internal structure. This matches how mathematicians actually think: isomorphic groups are 'one group', homotopy-equivalent spaces are 'one space'. Univalence makes this intuition formally correct. Computer verification (Lean, Agda) allows automatically checking the correctness of multi-page proofs.

Key Ideas

• **Types = spaces:** elements = points, p: a = b = paths; h-levels of types correspond to topological complexity
• **Univalence axiom:** A ≃ B ↔ A = B; isomorphic objects are identical - theorems transfer automatically
• **HITs:** path and homotopy constructors define CW complexes; S¹ = {base, loop}, T² = {pt, p, q, face}
• **HoTT as foundation:** ∞-groupoids as types; formal verification in Lean/Agda/Coq; alternative to ZFC for modern geometry

Related Topics

HoTT is a synthesis of topology, logic, and the theory of computation:

• CW Complexes — Higher inductive types are exactly CW complexes inside type theory; each cell = a constructor
• Covering Spaces — π₁(S¹) = Z is proved in HoTT via the recursion principle for S¹; coverings = families of types over S¹
• Topological Quantum Computing — In both theories paths are key objects: world lines of anyons in TQC, proofs of equality in HoTT

Вопросы для размышления

• If equality in HoTT is a path, what is a 'set' (h-level 0) - a space in which all paths are equal?
• How does the univalence axiom affect classical theorems that rely on specific representations of objects (e.g., real numbers as Cauchy sequences)?
• Can all of modern differential geometry be formulated inside HoTT? What does 'smoothness' mean for types?

Связанные уроки

• aa-03-homomorphisms