Voevodsky’s Univalence Axiom in Homotopy Type Theory


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



    Upload a copy of this work     Papers currently archived: 91,252

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

Identity in HoTT, Part I.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
Axiomatic Method and Category Theory.Rodin Andrei - 2013 - Cham: Imprint: Springer.
Combinatorial realizability models of type theory.Pieter Hofstra & Michael A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):957-988.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.


Added to PP

26 (#580,768)

6 months
6 (#448,852)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Steve Awodey
Carnegie Mellon University

Citations of this work

What is a Higher Level Set?Dimitris Tsementzis - 2016 - Philosophia Mathematica:nkw032.

Add more citations

References found in this work

No references found.

Add more references