الانتقال إلى المحتوى
The Lumenary
مسارات البحثFoundationsمُخطَّط له

Homotopy type theory

Homotopy type theory reads types as spaces (∞-groupoids) and equalities as paths. Voevodsky's univalence axiom identifies equivalent types, and higher inductive types make synthetic homotopy theory possible.

math.found.homotopy-type-theory

أظهِر كل ما يلزم للوصول إلى هذا الموضوع

لم يُكتب درس هذا الموضوع بعد. المخطط أدناه جزء من خريطة المنهج ولم تجرِ مراجعته.

يعتمد على

Type theory and propositions as typesAlgebraic topology

عدد المتطلبات السابقة الإلزامية (حتى الأساس): 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.

اكتشافات اختيارية

قراءات إضافية