Homotopy Type Theory — Foundations¶
Job: Fix Martin-Löf type theory as substrate; treat identity types as paths; state univalence; point to HITs and the \(\infty\)-groupoid interpretation; sample synthetic homotopy.
Core¶
Martin-Löf type theory (MLTT)¶
Judgments: \(\Gamma\ \mathsf{ctx}\), \(\Gamma\vdash A\ \mathsf{type}\), \(\Gamma\vdash a:A\), \(\Gamma\vdash a\equiv b:A\) (definitional equality).
| Former | Intro | Elim (computation) |
|---|---|---|
| \(\Pi_{x:A}B(x)\) | \(\lambda x.\,b\) | \(\mathrm{app}(f,a)\) |
| \(\Sigma_{x:A}B(x)\) | \((a,b)\) | \(\mathrm{ind}_\Sigma\) / projections |
| \(A+B\) | \(\mathsf{inl},\mathsf{inr}\) | case analysis |
| \(\mathbf{0},\mathbf{1},\mathbf{2}\) | — / \(\star\) / \(0_{\mathbf{2}},1_{\mathbf{2}}\) | absurd / unit / bool elim |
| \(\mathbb{N}\) | \(0\), \(\mathsf{suc}\) | primitive recursion |
| \(\mathcal{U}_i\) | universe hierarchy | types as terms of \(\mathcal{U}_i\) |
Propositions as types: a proof of \(A\) is a term \(a:A\). Dependent types express \(\forall\)/\(\exists\) via \(\Pi\)/\(\Sigma\). Function extensionality is not automatic in bare MLTT; follows from univalence (or is added).
Homotopy levels (h-levels):
| Level | Name | Meaning |
|---|---|---|
| \(-2\) | contractible | \(\sum_{x:A}\prod_{y:A}(y=x)\) |
| \(-1\) | proposition (h-prop) | all elements equal (prop. trunc.) |
| \(0\) | set (h-set) | identity types are props (UIP for that type) |
| \(1\) | groupoid | identities are sets; etc. |
Identity types as paths¶
For \(a:A\), identity type \(\mathrm{Id}_A(a,b)\) or \(a=_A b\). Reflexivity \(\mathsf{refl}_a:a=a\).
Path induction (J). To prove/construct \(C(x,p)\) for \(x:A\), \(p:a=x\), it suffices to give \(c:C(a,\mathsf{refl}_a)\). Computational rule: \(J(c,a,\mathsf{refl})\equiv c\).
Higher structure: \(p=_{a=b}q\) are homotopies; \(\Omega(A,a):=(a=a)\) is the loop space. Transport: \(p:a=b\) induces \(p_*:B(a)\to B(b)\) for \(B:A\to\mathcal{U}\).
Based path induction / Paulin-Mohring: often more convenient computationally. Groupoid laws (inverses, concatenation) hold up to higher paths — not judgmentally in intensional MLTT.
Univalence¶
An equivalence \(A\simeq B\) is a map with contractible fibers (or quasi-inverse with homotopies; coherent variants). Map $$ \mathsf{idtoequiv}:(A=_{\mathcal{U}}B)\to(A\simeq B) $$ sends \(\mathsf{refl}\) to \(\mathrm{id}\).
Univalence axiom (Voevodsky). \(\mathsf{idtoequiv}\) is itself an equivalence: $$ (A=_{\mathcal{U}}B)\;\simeq\;(A\simeq B). $$ Inverse \(\mathsf{ua}:(A\simeq B)\to(A=B)\). Consequences: function extensionality; transport along \(\mathsf{ua}(e)\) is the underlying map of \(e\); isomorphic structures are identified in the universe.
Higher inductive types (pointer)¶
HITs freely generate types with point and path constructors (and higher).
| HIT | Constructors |
|---|---|
| \(S^1\) | \(\mathsf{base}\), \(\mathsf{loop}:\mathsf{base}=\mathsf{base}\) |
| Suspension \(\Sigma A\) | poles + meridians |
| Pushout | points of summands + path constructors for diagram |
| Set quotient \(A/R\) | points + paths for relations + 0-truncation |
| Propositional truncation \(\|A\|\) | points of \(A\) + all paths |
Enable synthetic CW complexes, homotopy colimits, and quotients without choosing representatives.
\(\infty\)-groupoid interpretation¶
Homotopy hypothesis / semantic reading: a type \(A\) behaves as an \(\infty\)-groupoid — objects are terms, 1-morphisms are paths, \(k\)-morphisms are \(k\)-fold identities. Weak equivalences of spaces correspond to type-theoretic equivalences.
Models: simplicial sets (Kan) model of univalent type theory (Voevodsky); more generally \(\infty\)-toposes support univalent universes (Shulman et al.). Cubical type theory gives computational meaning to univalence (Kan operations on cubes) and implements HITs more directly.
Synthetic homotopy theory¶
Work inside type theory with HITs + univalence:
- \(\pi_1(S^1,{\mathsf{base}})\simeq\mathbb{Z}\) (encode winding via encode–decode)
- Freudenthal suspension, Blakers–Massey (formalized)
- Long exact sequences of homotopy groups for fibrations (fiber sequences as dependent types)
- Eilenberg–MacLane spaces \(K(G,n)\) as HITs; cohomology synthetic definitions
Point: classical homotopy theorems become type-theoretic constructions with explicit computational content where cubical / higher inductive computation applies.
See it¶
Encode–decode for \(\pi_1(S^1)\). Define \(F:\mathbb{N}\to\mathcal{U}\)? Better: family \(C:S^1\to\mathcal{U}\) with \(C(\mathsf{base})=\mathbb{Z}\) and transport around \(\mathsf{loop}\) \(=\) successor. Then \(\mathsf{encode}:(\mathsf{base}=_{S^1}x)\to C(x)\) by transport; \(\mathsf{decode}:\mathbb{Z}\to\Omega S^1\) by iterating \(\mathsf{loop}\). Prove mutual inverses — this is the template for computing homotopy groups synthetically.
Structure identity principle. For algebraic structures formalized as \(\Sigma\)-types of carriers + axioms (as props), univalence \(\Rightarrow\) isomorphisms of structures induce equalities of structured types — formalizes “isomorphism invariant mathematics.”
Check¶
Sketch why univalence implies function extensionality.
For \(f,g:A\to B\), a homotopy \(f\sim g\) yields a fiberwise equivalence between graphs / use that \(B^A\) classifies maps and ua identifies pointwise equivalent families; standard proof: consider the type family over \(\mathbf{2}\) interpolating \(f\) and \(g\) when they are homotopic, apply ua in a total space, project. (HoTT Book §4.9.)
Is every type an h-set in HoTT?
No. \(S^1\) has \(\Omega(S^1)\simeq\mathbb{Z}\not\simeq\mathbf{1}\); universe \(\mathcal{U}\) has nontrivial automorphisms. UIP is an extra axiom incompatible with full univalence.
Pitfalls¶
- Axiom vs computation: univalence as axiom blocks canonicity in plain MLTT; cubical models restore canonicity for a univalent system.
- Choice and LEM: AC/LEM at higher types imply all types are sets (or collapse higher structure) in univalent foundations; use carefully, prefer propositional AC.
- “Path = continuous map \([0,1]\to X\)” is only semantic; in syntax paths are inhabitants of identity types, not functions from an interval type unless interval is primitive (cubical).
- Strict vs weak: HIT path constructors satisfy laws up to higher paths; coherence obligations grow with dimension.
Refs¶
HoTT Book (IAS Univalent Foundations); Rijke, Introduction to Homotopy Type Theory; Awodey–Warren (identity types as paths); Voevodsky (univalence); Cohen–Coquand–Huber–Mörtberg (cubical TT); Shulman, All \((\infty,1)\)-toposes have strict univalent universes.
Next¶
Index · Logic · Category theory · Algebraic topology · Topos theory