Skip to Main Content

Bulletin of the American Mathematical Society

The Bulletin publishes expository articles on contemporary mathematical research, written in a way that gives insight to mathematicians who may not be experts in the particular topic. The Bulletin also publishes reviews of selected books in mathematics and short articles in the Mathematical Perspectives section, both by invitation only.

ISSN 1088-9485 (online) ISSN 0273-0979 (print)

The 2020 MCQ for Bulletin of the American Mathematical Society is 0.84.

What is MCQ? The Mathematical Citation Quotient (MCQ) measures journal impact by looking at citations over a five-year period. Subscribers to MathSciNet may click through for more detailed information.


Homotopy type theory and Voevodsky’s univalent foundations
HTML articles powered by AMS MathViewer

by Álvaro Pelayo and Michael A. Warren PDF
Bull. Amer. Math. Soc. 51 (2014), 597-648 Request permission


Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened homotopy type theory. In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the Univalence Axiom, which has a number of striking consequences. He has subsequently advocated a program, which he calls univalent foundations, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to homotopy type theory in Voevodsky’s setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky’s work using the well-known proof assistant Coq. The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science. Because a defining characteristic of Voevodsky’s program is that the Coq code has fundamental mathematical content, and many of the mathematical concepts which are efficiently captured in the code cannot be explained in standard mathematical English without a lengthy detour through type theory, the later sections of this paper (beginning with Section \ref{sec2}) make use of code; however, all notions are introduced from the beginning and in a self-contained fashion.
Similar Articles
Additional Information
  • Álvaro Pelayo
  • Affiliation: Department of Mathematics, University of California San Diego, 9500 Gilman Drive 0112, La Jolla, California 92093-0112
  • MR Author ID: 731609
  • Email:
  • Michael A. Warren
  • Affiliation: Los Angeles, California
  • Email:
  • Received by editor(s): October 20, 2012
  • Published electronically: May 9, 2014
  • Additional Notes: The first author was partly supported by NSF CAREER Award DMS-1055897, Spain Ministry of Science Grant MTM 2010-21186-C02-01, and Spain Ministry of Science Sev-2011-0087. He also received support from NSF Grant DMS-0635607 during the preparation of this paper.
    The second author received support from the Oswald Veblen Fund and NSF Grant DMS-0635607 during the preparation of this paper.
  • © Copyright 2014 American Mathematical Society
  • Journal: Bull. Amer. Math. Soc. 51 (2014), 597-648
  • MSC (2010): Primary 03-02; Secondary 03-B15, 68N18, 55P99
  • DOI:
  • MathSciNet review: 3237761