Homotopy Type Theory: Univalent Foundations of Mathematics

Peter Aczel Benedikt Ahrens Thorsten Altenkirch 1 Steve Awodey Bruno Barras Andrej Bauer Yves Bertot 2 Marc Bezem Thierry Coquand 3 Eric Finster Daniel Grayson Hugo Herbelin 4, 5 André Joyal Dan Licata Peter Lumsdaine Assia Mahboubi 6 Per Martin-Löf Sergey Melikhov Alvaro Pelayo 7 Andrew Polonsky Michael Shulman Matthieu Sozeau 4, 5 Bas Spitters 8 Benno Van den Berg Vladimir Voevodsky Michael Warren Carlo Angiuli Anthony Bordg Guillaume Brunerie Chris Kapulkin Egbert Rijke Kristina Sojakova Jeremy Avigad Cyril Cohen 3 Robert Constable Pierre-Louis Curien 4, 5 Peter Dybjer 3 Martín Escardó Kuen-Bang Hou Nicola Gambino Richard Garner 9 Georges Gonthier 10 Thomas Hales Robert Harper Martin Hofmann 11 Pieter Hofstra Joachim Koch Nicolai Kraus Nuo Li Zhaohui Luo Michael Nahas Erik Palmgren Emily Riehl Dana Scott Philip Scott Sergei Soloviev 12
Abstract : Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy the- ory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory; while type theory is a branch of mathematical logic and theoretical computer science. Although the connections between the two are currently the focus of intense investigation, it is increasingly clear that they are just the beginning of a subject that will take more time and more hard work to fully understand. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids.
Type de document :
Ouvrage (y compris édition critique et traduction)
Aucun, pp.448, 2013
Liste complète des métadonnées

Contributeur : Yves Bertot <>
Soumis le : jeudi 23 janvier 2014 - 00:56:04
Dernière modification le : jeudi 9 février 2017 - 15:47:43


  • HAL Id : hal-00935057, version 1



Peter Aczel, Benedikt Ahrens, Thorsten Altenkirch, Steve Awodey, Bruno Barras, et al.. Homotopy Type Theory: Univalent Foundations of Mathematics. Aucun, pp.448, 2013. <hal-00935057>



Consultations de la notice