PaperlayerView exact revision on arXiv

Source-linked AI summary

Homotopy Type Theory: Univalent Foundations of Mathematics

The Univalent Foundations Program

arXiv:1308.0729v1math.LOcs.PLmath.ATmath.CT

TL;DR

Classical set-theoretic foundations do not directly capture univalence and higher inductive types. This book presents homotopy type theory as a systematic, human-readable exposition and illustrates its constructive reasoning with homotopy-theoretic calculations.

  • Problem

    Classical set-theoretic foundations cannot directly capture univalence and higher inductive types, limiting their use for homotopical foundations.

  • Method

    The book interprets types as spaces or higher groupoids, develops homotopy-invariant constructions directly, and presents material originally developed through formal proof assistance.

  • Results

    The book develops a constructive calculation of π4(S3) without additional axioms, although the value k = 2 had not yet been checked.

  • Takeaways & Limitations

    Homotopy type theory provides a logic for manipulating spaces directly and supports proofs that could be computationally verified.

Abstract

from arXiv · show

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

IAS Special Year on Univalent Foundations

The Special Year on Univalent Foundations was held at the Institute for Advanced Study in 2012–13 and organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky. The book grew from collaborative efforts to develop human-readable informal type theory alongside machine-checkable formal proofs.

  • Special Year: The 2012–13 Special Year on Univalent Foundations took place at the Institute for Advanced Study, School of Mathematics, organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky.The event included official participants, students, and short- and long-term visitors.
  • Book Origins: The book originated in collective efforts to develop an informal type theory readable by humans as a complement to formal proofs checked by machines.Its formalization in a computer proof assistant was closely tied to univalent foundations, although it was not part of the book.
  • Collaboration: The Special Year’s participants contributed ideas, words, or deeds to the book within an unusually collaborative working spirit.The passage describes this collaboration as extraordinary.

9 Category theory

Section 9 develops category theory through categories and precategories, functors and transformations, adjunctions, equivalences, and the Yoneda lemma.

  • 9.1 Categories and precategories: The section begins with categories and precategories.
  • 9.2–9.4: It then introduces functors and transformations, followed by adjunctions and equivalences.
  • 9.5 The Yoneda lemma: The section concludes with the Yoneda lemma.

10 Set theory

The section develops set theory through the category of sets, cardinal and ordinal numbers, classical well-orderings, and the cumulative hierarchy.

  • 10 Set theory: The section begins with the category of sets and then treats cardinal and ordinal numbers.These topics are covered in Sections 10.1–10.3.
  • 10 Set theory: It concludes with classical well-orderings and the cumulative hierarchy.These topics are covered in Sections 10.4–10.5.

11 Real numbers

Section 11 develops real numbers through the field of rational numbers, Dedekind reals, and Cauchy reals. It then compares the two real-number constructions and studies compactness of the interval.

  • Real numbers: The section covers the field of rational numbers, Dedekind reals, and Cauchy reals.These topics appear as Sections 11.1–11.3, beginning on pages 364, 364, and 371, respectively.
  • Real numbers: It compares Cauchy and Dedekind reals and examines compactness of the interval.The comparison begins on page 389; the compactness subsection follows in the section outline.

Appendix · A Formal type theory

The appendix formally presents the type theory underlying the book, including its syntax, typing rules, universes, type formers, and metatheory. It then identifies function extensionality, univalence, and higher inductive types as the additional axioms distinguishing homotopy type theory from standard Martin-Löf type theory.

  • A.1 The first presentation: The first presentation defines terms through variables, constants, λ-abstraction, application, substitution, binding, convertibility, and judgmental equality.It also includes explicit definitions and total recursive definitions by structural recursion.
  • A.1.1 Type universes: The formal system postulates a cumulative hierarchy of universes U0, U1, U2, . . . and permits replacing equal types within typing judgments.The universe rules ensure that types inhabit some universe and that universe membership is cumulative.
  • A.1 The first presentation: The first presentation introduces dependent functions, dependent pairs, coproducts, finite types, natural numbers, W-types, and identity types with formation, construction, elimination, and computation rules.Natural numbers and W-types support primitive or total recursive definitions, while identity types include reflexivity and an elimination rule.
  • A.2 The second presentation: The second presentation recasts the theory as a deductive system of judgments derived by inference rules organized around contexts, structural principles, universes, and independently specified type formers.Each type former is systematically described by formation, introduction, elimination or induction, computation, and optional uniqueness rules.
  • A.3 Homotopy type theory: The homotopy type theory section adds function extensionality, the univalence axiom, and higher inductive types to standard Martin-Löf type theory.These are stated as the additional axioms distinguishing homotopy type theory from the standard system.
  • A.4 Basic metatheory: The Appendix A.1 system is logically consistent, has canonicity for natural numbers, and has decidable proofhood.A term of type 0 cannot exist in the empty context, while a closed natural number simplifies to succ^k(0) for some numeral k.
  • A.4 Basic metatheory: Consistency proofs for Martin-Löf type theory extended with univalence and higher inductive types currently proceed through semantic models rather than an appropriate normalization procedure.The cited models include Kan complexes for univalence and a model by Lumsdaine and Shulman for higher inductive types.

Index 447 · Introduction

Homotopy type theory combines homotopy theory and type theory, introducing univalence and higher inductive types into mathematical foundations. The Univalent Foundations program develops this perspective while remaining a young, evolving project presented as a snapshot of the field.

  • Introduction: Homotopy type theory combines homotopy theory with type theory, linking algebraic topology, homological algebra, higher category theory, mathematical logic, and theoretical computer science.The field is described as a new branch of mathematics based on a recently discovered connection between homotopy theory and type theory.
  • Introduction: The univalence axiom implies that isomorphic structures can be identified, bringing a foundational principle into homotopy type theory.The passage characterizes univalence as Voevodsky’s subtle and beautiful axiom.
  • Introduction: Higher inductive types provide direct, logical descriptions of constructions from homotopy theory.They are presented as the complementary foundational development alongside univalence.
  • Introduction: The Univalent Foundations program proposes foundations with intrinsic homotopical content, an invariant conception of mathematical objects, and convenient machine implementations.These implementations are intended to serve as a practical aid to the working mathematician.
  • Introduction: The book offers a first systematic exposition of univalent foundations and examples of its reasoning without requiring formal logic or computer-proof-assistant expertise.The supplied passage identifies the book’s purpose as explaining the basics and collecting examples of the new style of reasoning.
  • Introduction: Homotopy type theory is a young field, and univalent foundations remains a work in progress rather than an established, polished edifice.The book is described as a snapshot of the field when written, with aspects that are not yet fully understood.

Type theory

Type theory classifies objects by structured types whose predictable construction and decomposition support rigorous reasoning, program verification, and computer-assisted proof. Homotopy type theory reframes types as spaces, using homotopy theory to clarify their mathematical meaning and equality.

  • Type theory: Type theory classifies objects through primitive, structured types rather than sets, with type structure specifying how objects are constructed and decomposed.For a product type A × B, objects have the form (a, b), making their construction and decomposition immediate.
  • Type theory: Predictable behavior and clear reasoning principles make type theory useful for verifying computer programs and formalizing mathematics in proof assistants.These applications follow from rigid object formation and the construction principles associated with types.
  • Homotopy perspective: Homotopy type theory proposes understanding types as spaces viewed through homotopy theory, addressing longstanding difficulty in interpreting types mathematically.This perspective is presented as a significant step toward clarifying how equality of types should be understood.
  • Homotopy perspective: Homotopy theory studies spaces and continuous maps up to homotopy, where a homotopy continuously deforms one map into another.A homotopy H between f and g maps X × [0, 1] to Y and satisfies H(x, 0) = f(x) and H(x, 1) = g(x).
  • Homotopy perspective: Homotopy-equivalent spaces share algebraic invariants and are treated as having the same homotopy type.The equivalence is defined by maps in both directions whose composites are homotopic to the respective identity mappings.

Homotopy type theory

Homotopy type theory interprets types as spaces or ∞-groupoids and logical constructions as homotopy-invariant operations, enabling direct manipulation of spaces. Its key conceptual shift identifies equality with paths, while univalence adds a crucial property with far-reaching consequences.

  • Homotopy type theory: Homotopy type theory treats types as spaces or higher groupoids and logical constructions as homotopy-invariant constructions on them.This permits direct manipulation of spaces without first developing point-set topology or a combinatorial replacement such as simplicial sets.
  • Homotopy type theory: Functions f : A → B are regarded as continuous maps from the space A to the space B.
  • Homotopy type theory: Types are treated purely homotopically, with paths between points and homotopies between paths rather than topological notions such as open subsets or sequence convergence.The more accurate description is that types are ∞-groupoids, or invariant objects.
  • Homotopy type theory: Identity a = b between objects of a type A is understood as the existence of a path from point a to point b in the space A.Correspondingly, identifications form a path space, and homotopic functions can be identified.
  • Homotopy type theory: Univalence is a crucial additional property recognized in the simplicial interpretation of type theory, and adding it as an axiom has far-reaching, natural, simplifying consequences.It also further strengthens the homotopical interpretation of type theory.

Higher inductive types

Higher inductive types extend inductive definitions from points to paths and higher paths, providing logical descriptions of familiar spaces. They also express major homotopy-theoretic constructions and support formal homotopy-group calculations when combined with univalence.

  • Higher inductive types: Higher inductively defined spaces are generated by points, paths, and higher paths, with spheres and the torus as examples.Classically, these spaces are called CW complexes.
  • Higher inductive types: Identifying paths with identities lets type theory characterize these spaces through induction principles, analogously to natural numbers and disjoint unions.This extends type theory’s established methods for inductively defined structures.
  • Higher inductive types: Higher inductive types provide a direct logical way to reason about spaces such as spheres and, with univalence, formally calculate their homotopy groups.These proofs combine classical homotopy-theoretic and type-theoretic ideas.
  • Higher inductive types: Higher inductive types can express homotopy colimits, suspensions, Postnikov towers, localization, completion, and spectrification.Many such constructions are classically built using Quillen’s small object argument to describe infinite CW complex presentations algorithmically.

Informal type theory

The section motivates an informal presentation of type theory for working mathematicians and emphasizes its practical implementation in proof assistants. It also reports that formalization can aid both the formalization and discovery of mathematical proofs.

  • Motivation: Type theory is often presented as a formalized deductive system, which is useful for proof theory but inconvenient and unfamiliar for informal mathematical reasoning.The work aims to develop a more accessible presentation for applied, informal reasoning.
  • Implementation: Formal type theory supports proof assistants that guide users through valid proof steps, automate tasks, search theorem libraries, and extract numerical algorithms.The system has been implemented in existing proof assistants.
  • Results: Proof assistants have demonstrated value not only by formalizing known proofs but also by discovering new ones.Many proofs in the book were first completed formally and only later converted into informal mathematics.
  • Future utility: The authors argue that univalent foundations could make verification of mathematicians’ own papers in proof assistants practically attainable.They envision this becoming as natural as typesetting papers in TEX.

Constructivity

Constructive type theory treats propositions as types and proofs as mathematical objects, giving existence and implication a computational meaning. Homotopy type theory can selectively recover classical principles while retaining constructive reasoning, and univalence and higher inductive types make several constructions directly constructive.

  • Constructive logic: Type theory represents propositions as types, so proofs are first-class objects and proving a statement amounts to constructing an inhabitant of its corresponding type.This proof-relevant interpretation underlies the computational character of type theory.
  • Constructive logic: Constructive proofs of conjunction, implication, and existence carry computational content: they provide pairs, functions, and witnesses rather than merely asserting that such objects exist.For example, proving A implies B constructs a function A → B, while proving existence constructs enough information to compute a witness.
  • Classical principles: Naive classical principles behave differently: the type-theoretic axiom of choice is constructively provable, whereas the law of excluded middle conflicts with univalence.Univalence rules out a uniform choice of elements from every nonempty type because such choices must be invariant under self-equivalences.
  • Classical principles: Homotopy type theory stratifies types by homotopy dimension, allowing propositions to support more traditional intuitionistic logic while general types remain constructive.The system can impose further classical principles only on selected truncated types, rather than on all types.
  • Classical principles: Univalent foundations can assume the proper truncated forms of excluded middle and choice, but avoiding them preserves applicability to nonstandard models and supports computation.Type theory is also a formal theory of computation, so its rules must support executing proofs as programs.
  • Constructive advantages: Univalence and higher inductive types replace several choice-dependent set-theoretic constructions with direct constructive ones, including categorical equivalences, cardinal representatives, and well-behaved real numbers.In particular, every fully faithful and essentially surjective functor is an equivalence under univalence, without the set-theoretic equivalence to choice.

Open problems

The open problems center on establishing the constructivity of the Univalence Axiom, handling essentially discrete types, clarifying connections with higher toposes, and formalizing everyday mathematics. Recent formalization successes are encouraging, but substantial work remains.

  • Constructivity: The most pressing question is whether the Univalence Axiom is constructive within type theory.Normalization underlies decidable type-checking and canonicity, motivating the importance of establishing comparable properties for univalence.
  • Discrete types: Homotopy type theory struggles to characterize essentially discrete spaces, such as natural numbers, beyond homotopy equivalence.This produces paths equal to reflexivity without being judgmentally equal to it.
  • Higher toposes: The relationship between homotopy type theory and higher topos research remains to be clarified, including correspondences involving univalent universes and higher inductive types.The proposed connections identify univalent universes with object classifiers and higher inductive types with elementary reflections of local phenomena.
  • Formalization: The largest remaining effort is formalizing everyday mathematics in the new system.Formalizations in basic homotopy theory and category theory have succeeded, but much work remains.

How to read this book

The book’s Foundations section develops the concepts needed for univalent foundations, while Mathematics applies them across four largely independent areas. Reading requirements vary by chapter, with Part I providing essential preparation but selected chapters allowing readers to proceed with less background.

  • Book structure: Part I develops the fundamental concepts required to understand univalent foundations, while Part II applies them in homotopy theory, category theory, set theory, and real analysis.Part I is extensive because the basic notions require acclimatization; Part II chapters are more or less independent.
  • Reading guidance: Readers seeking mastery must eventually understand most of Part I, whereas readers seeking an introduction can use each Part II chapter’s overview to identify the necessary background.Chapter 2 is especially encouraged for everyone, while Chapters 4–7 are more selectively useful depending on the Part II subject.
  • Part II: Mathematics: Chapter 8 presents a synthetic approach to homotopy theory in which types are basic homotopy objects, illustrating proofs from π1(S1) = Z through the Freudenthal suspension theorem.Homotopy types are not constructed from topological spaces or another set-theoretic model.
  • Part II: Mathematics: Chapter 9 develops category theory under the principle that equality is isomorphism, making definitions and constructions invariant under equivalence of categories.Equivalent categories are equal just as equivalent types are equal.
  • Part II: Mathematics: Chapter 10 studies sets, observes that univalence simplifies cardinal and ordinal numbers, and uses higher inductive types to obtain a cumulative hierarchy satisfying Zermelo–Fraenkel axioms.The category of sets retains its usual properties and supports mathematics without homotopical or higher-categorical structures.
  • Part II: Mathematics: Chapter 11 summarizes Dedekind real numbers and uses higher inductive types to define Cauchy reals while avoiding some constructive-mathematics problems, then sketches Conway’s surreal numbers.The chapter presents a similar higher-inductive approach for surreal numbers.

FOUNDATIONS · Type theory

The foundations present homotopy type theory as an alternative to set theory, replacing its two-layer structure with a single type-theoretic system that treats propositions as types. Its rules govern objects, computation, equality, contexts, and function formation, while propositions correspond naturally to types of witnesses.

  • 1.1 Type theory versus set theory: Homotopy type theory is an alternative foundational language to Zermelo–Fraenkel set theory, with important differences from set-theoretic foundations.These differences motivate a more formal comparison before returning to an informal presentation.
  • 1.1 Type theory versus set theory: Set theory combines first-order logic with axioms about sets, whereas type theory is a self-contained deductive system whose basic notion is type.Propositions are identified with particular types, so proving a theorem becomes a form of constructing an object.
  • 1.1 Type theory versus set theory: The judgment a : A states that an object or witness a has type A, paralleling membership while making each element inherently associated with a type.When A represents a proposition, a is evidence or a witness of its truth; when A behaves like a set, a : A is analogous to a ∈ A.
  • 1.1 Type theory versus set theory: Type theory distinguishes propositional equality a =_A b from judgmental or definitional equality a ≡ b, which expresses equality by definition.Judgmental equality controls typing: if a : A and A ≡ B, then a : B; for example, a proof about 3^2 can apply to f(3) when f(3) is definitionally 3^2.
  • 1.1 Type theory versus set theory: The system organizes reasoning through judgments, contexts of assumptions, type formers, and procedural rules, generally without axioms.Contexts may include typed variables and proof objects, and rules encode the behavior of constructions, supporting computational properties such as canonicity.
  • 1.2 Function types: Given types A and B, function types A → B are primitive constructions whose elements are functions, introduced by definitions or λ-abstraction and evaluated by substitution.Applying a λ-abstraction yields a definitional equality, and the uniqueness principle says a function is determined by its values.
  • 1.11 Propositions as types: Logical operations on propositions correspond naturally to type-theoretic operations on the associated types of witnesses.This correspondence underlies the identification of propositions with types.

Type Theory … Index

The paper develops homotopy type theory as a constructive foundation in which types carry intrinsic ∞-groupoid structure, while univalence identifies equivalent types and supports invariant reasoning about mathematical structures. It also presents inductive and higher inductive types as synthetic, computational descriptions of spaces and universal constructions.

  • Type Theory: Propositions-as-types translates propositions and proofs into types and elements, giving type-theoretic logic intrinsic computational meaning and freedom to add compatible assumptions such as LEM.Constructivity supplies computational content, while LEM has no default witnessing construction but may consistently be assumed.
  • Homotopy type theory: Each type forms an ∞-groupoid, with identity proofs as paths and higher identity proofs as paths between paths; identity-type induction generates the full higher-groupoid structure.Functions between types correspond to ∞-functors, and the presentation avoids requiring the full combinatorics of coherent higher structure.
  • Higher inductive types: Higher inductive types give synthetic descriptions of spaces by specifying points, paths, and higher constructors, though concrete descriptions of their identity types can be nontrivial.The circle has a nontrivial loop, and its universe cannot be a 1-type because the circle has nontrivial higher equality structure.
  • 2.5 The higher groupoid structure of type formers: Univalence states that equivalent types are equal, making semigroups equal precisely when they are isomorphic and causing mathematical constructions to respect isomorphisms automatically.The same framework derives function extensionality from univalence.
  • Homotopy theory: The development connects type theory with classical mathematical constructions through product paths, coproduct and natural-number identity codes, object classifiers, universal properties, and synthetic sphere constructions.These results identify paths in products componentwise, characterize coproduct and natural-number equalities, and establish expected universal behavior for spheres.
  • Sets and logic: The propositions-as-types viewpoint distinguishes mere propositions from data-bearing types, explains propositional truncation, and shows that univalence is incompatible with unrestricted double negation and excluded middle.Mere propositions are sets, while propositional truncation retains only whether a disjunction holds, not which disjunct witnesses it.
  • Equivalences: Equivalences admit multiple pairwise equivalent definitions and satisfy closure principles including surjective-and-embedding characterization, 2-out-of-3, and stability under retracts and fiberwise transformations.Contractible fibers provide another equivalent characterization, and all three principal definitions meet the desired equivalence properties.
  • Induction: Inductive types are characterized by their induction and computation principles: types satisfying the same principles are equivalent and, by univalence, equal, while inductive types serve as homotopy-initial algebras.Natural numbers and W-types exemplify this characterization, and homotopy-inductive formulations replace definitional computation rules with propositional ones.
Loading 1308.0729v1…