An introduction to univalent foundations for mathematicians

TL;DR

This paper introduces univalent foundations, a new approach to mathematical foundations based on type theory, highlighting its potential as a comprehensive alternative to traditional set theory.

Contribution

It provides an accessible introduction for mathematicians to Voevodsky's univalent foundations and explains how they can encode all of modern mathematics.

Findings

Univalent foundations can serve as a viable alternative to set theory.

Type theory encodes mathematics in a way that reveals new foundational insights.

The approach offers a potentially unified foundation for all of mathematics.

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.