Homotopy type theory

前置知识

50 项必需的前置知识（一直追溯到底）

你将学会

• Explain identity types and their path interpretation, including transport and path induction.
• State the univalence axiom and explain why it is incompatible with uniqueness of identity proofs for the universe.
• Define the circle as a higher inductive type and outline the synthetic proof that its loop space is equivalent to ℤ.

定义

• For a, b : A, the identity type a =_A b has elements thought of as paths from a to b.
• An equivalence of types is a function with contractible fibres, equivalently one with a two-sided homotopy inverse.
• Univalence: for types A and B in a universe, the canonical map (A = B) → (A ≃ B) is an equivalence.
• A higher inductive type has constructors for paths as well as points, such as base : S¹ and loop : base = base.

定理

• In homotopy type theory the loop space of the circle is equivalent to ℤ (Licata and Shulman).
• Univalence implies function extensionality.
• Univalent type theory has a model in Kan simplicial sets (Kapulkin and Lumsdaine, after Voevodsky).

常见误解

• Thinking HoTT replaces set theory or category theory wholesale; it is one foundation among several, with its own strengths and open questions.
• Reading univalence as a statement about sets in ZFC; it is an axiom about identity types inside type theory.
• Identifying HoTT with ∞-category theory; they are connected through models, not the same subject.

可选发现

• ∞-categories Shulman (2019) showed that every Grothendieck (∞,1)-topos gives a model of homotopy type theory with univalent universes.
• ← Homotopy and the fundamental group
• ← The Yoneda lemma
• ← Categorical logic
• ← Higher categories

延伸阅读

• The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics (2013)