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)