# Homotopy Type Theory: Univalent Foundations of Mathematics

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.

- 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

- 1 Type theory
- 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

- 8.1 π₁(S¹)
- 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

- 10.1 The category of sets
- 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

- 8 Homotopy theory
- 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

- A.1 The first presentation

- A Formal type theory
- Bibliography
- Index of symbols
- Index

#### Free Machine Learning Books

11 Books

- 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

#### Free Chemistry Textbooks

9 Books

- CK-12 Chemistry
- by Various
- Concept Development Studies in Chemistry
- by John Hutchinson
- An Introduction to Chemistry - Atoms First
- by Mark Bishop

#### Free Mathematics Textbooks

21 Books

- Microsoft Word - How to Use Advanced Algebra II.doc
- by Jonathan Emmons
- Advanced Algebra II: Activities and Homework
- by Kenny Felder
- de2de
- by

#### Free Children Books

38 Books

- The Sun Who Lost His Way
- by
- Tania is a Detective
- by Kanika G
- Firenze_s-Light
- by

#### Free Java Books

10 Books

- Java 3D Programming
- by Daniel Selman
- The Java EE 6 Tutorial
- by Oracle Corporation
- JavaKid811
- by