Voevodsky’s Univalence Axiom in Homotopy Type Theory

, &

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

Categories

Keywords

Reprint years

Links

PhilArchive



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

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.

My notes

Similar books and articles

Homotopy theoretic models of identity types.Steve Awodey & Michael A. Warren - unknown
Reviewed Work: Homotopy Type Theory: Univalent Foundations of Mathematics, http://homotopytypetheory.org/book, Institute for Advanced Study The Univalent Foundations Program.Review by: Jaap van Oosten - 2014 - Bulletin of Symbolic Logic 20 (4):497-500,.
Identity in Homotopy Type Theory, Part I: The Justification of Path Induction.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
Natural models of homotopy type theory.Steve Awodey - unknown
Homotopy limits in type theory.Jeremy Avigad, Krzysztof Kapulkin & Peter Lefanu Lumsdaine - unknown
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.
Mathematical Forms and Forms of Mathematics: Leaving the Shores of Extensional Mathematics.Jean-Pierre Marquis - 2013 - Synthese 190 (12):2141-2164.
Type Theory and Homotopy.Steve Awodey - unknown
Combinatorial realizability models of type theory.Pieter Hofstra & Michael A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):957-988.
A Primer on Homotopy Type Theory Part 1: The Formal Type Theory.James Ladyman & Stuart Presnell - unknown
Characterizing the interpretation of set theory in Martin-Löf type theory.Michael Rathjen & Sergei Tupailo - 2006 - Annals of Pure and Applied Logic 141 (3):442-471.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
An interpretation of Martin-löf's type theory in a type-free theory of propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.

Analytics

Added to PP
2016-01-18

Downloads
25 (#581,490)

6 months
5 (#441,012)

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