Voevodsky's Univalence Axiom in homotopy type theory
History and Overview
2013-02-20 v1 Logic
Abstract
In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky's univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.
Keywords
Cite
@article{arxiv.1302.4731,
title = {Voevodsky's Univalence Axiom in homotopy type theory},
author = {Steve Awodey and Álvaro Pelayo and Michael A. Warren},
journal= {arXiv preprint arXiv:1302.4731},
year = {2013}
}
Comments
To appear in Notices of the American Mathematical Society