Remote Access Bulletin of the American Mathematical Society

Bulletin of the American Mathematical Society

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

   
 
 

 

An introduction to univalent foundations for mathematicians


Author: Daniel R. Grayson
Journal: Bull. Amer. Math. Soc.
MSC (2010): Primary 03B35, 03B15
DOI: https://doi.org/10.1090/bull/1616
Published electronically: March 5, 2018
Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: We offer an introduction for mathematicians to the univalent foundations of Vladimir Voevodsky, aiming to explain how he chose to encode mathematics in type theory and how the encoding reveals a potentially viable foundation for all of modern mathematics that can serve as an alternative to set theory.


References [Enhancements On Off] (What's this?)


Similar Articles

Retrieve articles in Bulletin of the American Mathematical Society with MSC (2010): 03B35, 03B15

Retrieve articles in all journals with MSC (2010): 03B35, 03B15


Additional Information

Daniel R. Grayson
Affiliation: 2409 S. Vine St., Urbana, Illinois 61801
Email: drg@illinois.edu

DOI: https://doi.org/10.1090/bull/1616
Keywords: Homotopy type theory, type theory, identity type, univalence axiom, univalent mathematics
Received by editor(s): February 7, 2018
Published electronically: March 5, 2018
Article copyright: © Copyright 2018 Daniel R. Grayson

American Mathematical Society