Homotopy Type Theory: Univalent Foundations of Mathematics
Free

Homotopy Type Theory: Univalent Foundations of Mathematics

By The Univalent Foundations Program, Institute for Advanced Study
Free
Book Description

Homotopy type theory is a new branch of mathematics that combines
aspects of several different fields in a surprising way. It is based on a
recently discovered connection between homotopy theory and type theory.
It touches on topics as seemingly distant as the homotopy groups of
spheres, the algorithms for type checking, and the definition of weak
∞-groupoids. Homotopy type theory offers a new “univalent” foundation of
mathematics, in which a central role is played by Voevodsky’s
univalence axiom and higher inductive types. The present book is
intended as a first systematic exposition of the basics of univalent
foundations, 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. We believe that univalent
foundations will eventually become a viable alternative to set theory as
the “implicit foundation” for the unformalized mathematics done by most
mathematicians.


This is the first (and to date, only) edition of the book. For the benefit of all readers, the available PDF and printed copies are being updated on a rolling basis with minor corrections and clarifications as we receive them. Every copy has a version marker that can be found on the title page and is of the form “first-edition-XX-gYYYYYYY”, where XX is a natural number and YYYYYYY is the git commit hash that uniquely identifies the exact version. Higher values of XX indicate more recent copies. This update was on August 30, 2015 and its version marker is "first-edition-967-g0b0914e". The most recent builds, as well as PDFs with other form factors are available on GitHub. Printed copies may be purchased via the books homepage.

Table of Contents
  • Preface
  • Table of Contents
  • Introduction
  • I Foundations
    • 1 Type theory
      • 1.1 Type theory versus set theory
      • 1.2 Function types
      • 1.3 Universes and families
      • 1.4 Dependent function types (Π-types)
      • 1.5 Product types
      • 1.6 Dependent pair types (Σ-types)
      • 1.7 Coproduct types
      • 1.8 The type of booleans
      • 1.9 The natural numbers
      • 1.10 Pattern matching and recursion
      • 1.11 Propositions as types
      • 1.12 Identity types
        • 1.12.1 Path induction
        • 1.12.2 Equivalence of path induction and based path induction
        • 1.12.3 Disequality
      • Notes
      • Exercises
    • 2 Homotopy type theory
      • 2.1 Types are higher groupoids
      • 2.2 Functions are functors
      • 2.3 Type families are fibrations
      • 2.4 Homotopies and equivalences
      • 2.5 The higher groupoid structure of type formers
      • 2.6 Cartesian product types
      • 2.7 Σ-types
      • 2.8 The unit type
      • 2.9 Π-types and the function extensionality axiom
      • 2.10 Universes and the univalence axiom
      • 2.11 Identity type
      • 2.12 Coproducts
      • 2.13 Natural numbers
      • 2.14 Example: equality of structures
        • 2.14.1 Lifting equivalences
        • 2.14.2 Equality of semigroups
      • 2.15 Universal properties
      • Notes
      • Exercises
    • 3 Sets and logic
      • 3.1 Sets and n-types
      • 3.2 Propositions as types?
      • 3.3 Mere propositions
      • 3.4 Classical vs. intuitionistic logic
      • 3.5 Subsets and propositional resizing
      • 3.6 The logic of mere propositions
      • 3.7 Propositional truncation
      • 3.8 The axiom of choice
      • 3.9 The principle of unique choice
      • 3.10 When are propositions truncated?
      • 3.11 Contractibility
      • Notes
      • Exercises
    • 4 Equivalences
      • 4.1 Quasi-inverses
      • 4.2 Half adjoint equivalences
      • 4.3 Bi-invertible maps
      • 4.4 Contractible fibers
      • 4.5 On the definition of equivalences
      • 4.6 Surjections and embeddings
      • 4.7 Closure properties of equivalences
      • 4.8 The object classifier
      • 4.9 Univalence implies function extensionality
      • Notes
      • Exercises
    • 5 Induction
      • 5.1 Introduction to inductive types
      • 5.2 Uniqueness of inductive types
      • 5.3 W-types
      • 5.4 Inductive types are initial algebras
      • 5.5 Homotopy-inductive types
      • 5.6 The general syntax of inductive definitions
      • 5.7 Generalizations of inductive types
      • 5.8 Identity types and identity systems
      • Notes
      • Exercises
    • 6 Higher inductive types
      • 6.1 Introduction
      • 6.2 Induction principles and dependent paths
      • 6.3 The interval
      • 6.4 Circles and spheres
      • 6.5 Suspensions
      • 6.6 Cell complexes
      • 6.7 Hubs and spokes
      • 6.8 Pushouts
      • 6.9 Truncations
      • 6.10 Quotients
      • 6.11 Algebra
      • 6.12 The flattening lemma
      • 6.13 The general syntax of higher inductive definitions
      • Notes
      • Exercises
    • 7 Homotopy n-types
      • 7.1 Definition of n-types
      • 7.2 Uniqueness of identity proofs and Hedberg's theorem
      • 7.3 Truncations
      • 7.4 Colimits of n-types
      • 7.5 Connectedness
      • 7.6 Orthogonal factorization
      • 7.7 Modalities
      • Notes
      • Exercises
  • II Mathematics
    • 8 Homotopy theory
      • 8.1 π₁(S¹)
        • 8.1.1 Getting started
        • 8.1.2 The classical proof
        • 8.1.3 The universal cover in type theory
        • 8.1.4 The encode-decode proof
        • 8.1.5 The homotopy-theoretic proof
        • 8.1.6 The universal cover as an identity system
      • 8.2 Connectedness of suspensions
      • 8.3 π_(k≤n) of an n-connected space and π_(k<n)(Sⁿ)
      • 8.4 Fiber sequences and the long exact sequence
      • 8.5 The Hopf fibration
        • 8.5.1 Fibrations over pushouts
        • 8.5.2 The Hopf construction
        • 8.5.3 The Hopf fibration
      • 8.6 The Freudenthal suspension theorem
      • 8.7 The van Kampen theorem
        • 8.7.1 Naive van Kampen
        • 8.7.2 The van Kampen theorem with a set of basepoints
      • 8.8 Whitehead's theorem and Whitehead's principle
      • 8.9 A general statement of the encode-decode method
      • 8.10 Additional Results
      • Notes
      • Exercises
    • 9 Category theory
      • 9.1 Categories and precategories
      • 9.2 Functors and transformations
      • 9.3 Adjunctions
      • 9.4 Equivalences
      • 9.5 The Yoneda lemma
      • 9.6 Strict categories
      • 9.7 †-categories
      • 9.8 The structure identity principle
      • 9.9 The Rezk completion
      • Notes
      • Exercises
    • 10 Set theory
      • 10.1 The category of sets
        • 10.1.1 Limits and colimits
        • 10.1.2 Images
        • 10.1.3 Quotients
        • 10.1.4 Set is a ΠW-pretopos
        • 10.1.5 The axiom of choice implies excluded middle
      • 10.2 Cardinal numbers
      • 10.3 Ordinal numbers
      • 10.4 Classical well-orderings
      • 10.5 The cumulative hierarchy
      • Notes
      • Exercises
    • 11 Real numbers
      • 11.1 The field of rational numbers
      • 11.2 Dedekind reals
        • 11.2.1 The algebraic structure of Dedekind reals
        • 11.2.2 Dedekind reals are Cauchy complete
        • 11.2.3 Dedekind reals are Dedekind complete
      • 11.3 Cauchy reals
        • 11.3.1 Construction of Cauchy reals
        • 11.3.2 Induction and recursion on Cauchy reals
        • 11.3.3 The algebraic structure of Cauchy reals
        • 11.3.4 Cauchy reals are Cauchy complete
      • 11.4 Comparison of Cauchy and Dedekind reals
      • 11.5 Compactness of the interval
      • 11.6 The surreal numbers
      • Notes
      • Exercises
  • Appendix
    • A Formal type theory
      • A.1 The first presentation
        • A.1.1 Type universes
        • A.1.2 Dependent function types (Π-types)
        • A.1.3 Dependent pair types (Σ-types)
        • A.1.4 Coproduct types
        • A.1.5 The finite types
        • A.1.6 Natural numbers
        • A.1.7 W-types
        • A.1.8 Identity types
      • A.2 The second presentation
        • A.2.1 Contexts
        • A.2.2 Structural rules
        • A.2.3 Type universes
        • A.2.4 Dependent function types (Π-types)
        • A.2.5 Dependent pair types (Σ-types)
        • A.2.6 Coproduct types
        • A.2.7 The empty type 0
        • A.2.8 The unit type 1
        • A.2.9 The natural number type
        • A.2.10 Identity types
        • A.2.11 Definitions
      • A.3 Homotopy type theory
        • A.3.1 Function extensionality and univalence
        • A.3.2 The circle
      • A.4 Basic metatheory
      • Notes
  • Bibliography
  • Index of symbols
  • Index
    No review for this book yet, be the first to review.
      No comment for this book yet, be the first to comment
      Also Available On
      App store smallGoogle play small
      Categories
      Curated Lists
      • Pattern Recognition and Machine Learning (Information Science and Statistics)
        by Christopher M. Bishop
        Data mining
        by I. H. Witten
        The Elements of Statistical Learning: Data Mining, Inference, and Prediction
        by Various
        See more...
      • CK-12 Chemistry
        by Various
        Concept Development Studies in Chemistry
        by John Hutchinson
        An Introduction to Chemistry - Atoms First
        by Mark Bishop
        See more...
      • Microsoft Word - How to Use Advanced Algebra II.doc
        by Jonathan Emmons
        Advanced Algebra II: Activities and Homework
        by Kenny Felder
        de2de
        by
        See more...
      • The Sun Who Lost His Way
        by
        Tania is a Detective
        by Kanika G
        Firenze_s-Light
        by
        See more...
      • Java 3D Programming
        by Daniel Selman
        The Java EE 6 Tutorial
        by Oracle Corporation
        JavaKid811
        by
        See more...