An introduction to univalent foundations for mathematicians

2017/11/04 by Daniel R. Grayson · 1 voice
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #History and Theory of Mathematics #Logic, programming, and type systems #math.LO

paper · pdf · doi:10.1090/bull/1616

arxiv published 2017/11/04 · arxiv updated 2018/02/08 · openalex publication_date 2018/03/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Products of families of types in the C-systems defined by a universe category
• A formal proof of the four color theorem
• Univalence in Simplicial Sets
• A C-system defined by a universe category
• Computational Higher Type Theory I: Abstract Cubical Realizability
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
• On the homotopy groups of spheres in homotopy type theory
• Computational Higher Type Theory II: Dependent Cubical Realizability
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• The homotopy theory of type theories
• Mathematical Logic as Based on the Theory of Types
• The James construction and π₄(\mathbbS³) in homotopy type theory
• C-systems defined by universe categories: presheaves
• Homotopy type theory: the logic of space

Discussions

• An introduction to univalent foundations for mathematicians [pdf] [hn, 2 points, 0 comments]