An introduction to univalent foundations for mathematicians

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 in corpus (16)

• A formal proof of the four color theorem
• Homotopy theoretic models of identity types
• On the homotopy groups of spheres in homotopy type theory
• Computational Higher Type Theory I: Abstract Cubical Realizability
• Computational Higher Type Theory II: Dependent Cubical Realizability
• Goodwillie's Calculus of Functors and Higher Topos Theory
• Computational Higher Type Theory IV: Inductive Types
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
• Homotopy type theory: the logic of space
• Martin-Lof identity types in the C-systems defined by a universe category
• Products of families of types in the C-systems defined by a universe category
• C-systems defined by universe categories: presheaves
• Lawvere theories and Jf-relative monads
• Cellular Cohomology in Homotopy Type Theory
• The James construction and ${\pi }_4({\mathbb{S}}^3)$ in homotopy type theory
• Internal Languages of Finitely Complete $(\infty ,1)$-categories

Cited by in corpus (5)

• Automated Mathematics and the Reconfiguration of Proof and Labor
• A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom
• One Mathematic(s) or Many? Foundations of Mathematics in Today's Mathematical Practice
• The Role of General Intelligence in Mathematical Reasoning
• The Surreal Numbers as an Ordered Commutative Ring with an Apartness: A Development in Univalent Foundations