Homotopy Type Theory¶
Job: map HoTT as a foundation where types are spaces, identities are paths, and univalence equates equivalence with equality — synthetic homotopy + formalizable mathematics.
Core¶
HoTT extends Martin-Löf type theory with univalence and higher inductive types (HITs). The intended model: types \(\simeq\) \(\infty\)-groupoids / homotopy types; terms \(\simeq\) points; identity type \(x=y\) \(\simeq\) path space.
| Layer | Content |
|---|---|
| MLTT | \(\Pi\), \(\Sigma\), \(+\), \(\mathbf{0},\mathbf{1},\mathbb{N}\); dependent types |
| Identity types | path induction (J); higher paths |
| Univalence | \((A\simeq B)\simeq(A=_{\mathcal{U}}B)\) |
| HITs | \(S^1\), pushouts, truncations, quotients |
| Synthetic homotopy | \(\pi_1(S^1)=\mathbb{Z}\) inside type theory |
| Models | \(\infty\)-toposes; cubical type theory (computational) |
Reading map¶
| Page | Focus |
|---|---|
| Foundations | MLTT, paths, univalence, HITs pointer, \(\infty\)-groupoid reading, synthetic homotopy |
| Cubical & Computational | interval \(I\), Kan composition, canonicity, computational univalence |
| Synthetic Homotopy | encode-decode \(\pi_1(S^1)\), Freudenthal, Blakers–Massey, \(K(G,n)\), \(H^n\) |
| Models & Semantics | simplicial Voevodsky, \(\infty\)-topos Shulman, cubical presheaf, ZFC/constructive |
| Univalent Categories | Rezk completeness, directed type theory, SIP, Agda/Coq/Lean |
Dependency order¶
- Logic (proofs-as-programs intuition; quantifiers)
- Category theory (adjoints, universes of sets as topos baseline)
- Algebraic topology (homotopy groups, CW, weak equivalences)
- This section: type theory as synthetic homotopy
Where it appears¶
- Formalization of homotopy theory in proof assistants (Cubical Agda, Coq HoTT library)
- Constructive mathematics with homotopical equality
- Semantics of type theory in higher toposes
- Higher category theory as design space for foundations
See it¶
Univalence in practice. If \(A\simeq B\) via \(e\), transport along \(\mathsf{ua}(e)\) moves theorems about \(A\) to \(B\) automatically. “Isomorphic structures are equal” becomes a theorem schema — the formal counterpart of mathematical abuse of language, controlled by homotopy level (sets vs groupoids vs higher types).
Check¶
What is the difference between judgmental equality \(a\equiv b\) and propositional \(a=_A b\)?
Judgmental: definitional, computational, not data. Propositional: a type of witnesses (paths); can have nontrivial structure (\(\pi_1\), etc.). Conflation is the classic set-theoretic habit HoTT breaks.
Why does univalence contradict uniqueness of identity proofs (UIP)?
UIP says every identity type is a proposition (at most one path up to higher path). Univalence produces nontrivial loops in the universe (e.g. nontrivial automorphisms of a type become nontrivial self-equalities). So \(\mathcal{U}\) is not an h-set.
Pitfalls¶
- Prop vs Type: propositions-as-some-types (h-props) differ from plain MLTT “Prop” sugar; truncation is essential.
- Classical axioms: LEM at all types is homotopically bad; restricted LEM for propositions is the safe classical fragment.
- Interpretation: “types are spaces” is semantic; syntax remains type theory — not every topological construction is automatically internal.
Refs¶
The Univalent Foundations Program, Homotopy Type Theory (HoTT Book); Rijke notes; Cubical type theory papers (Cohen–Coquand–Huber–Mörtberg); Shulman surveys on \(\infty\)-topos models.
Next¶
Foundations · Logic · Category theory · Algebraic topology · Topos theory · Cubical & Computational · Synthetic Homotopy · Models & Semantics · Univalent Categories