Skip to Main content Skip to Navigation
New interface

Homotopy Type Theory: Univalent Foundations of Mathematics

Peter Aczel 1 Benedikt Ahrens 2 Thorsten Altenkirch 3 Steve Awodey 4 Bruno Barras 5 Andrej Bauer 6 Yves Bertot 7 Marc Bezem 8 Thierry Coquand 9 Eric Finster 5 Daniel Grayson 10 Hugo Herbelin 11, 12 André Joyal 8 Dan Licata 4 Peter Lumsdaine 13 Assia Mahboubi 14 Per Martin-Löf 15 Sergey Melikhov 16 Alvaro Pelayo 17 Andrew Polonsky 8 Michael Shulman 18 Matthieu Sozeau 11, 12 Bas Spitters 19 Benno van den Berg 20 Vladimir Voevodsky 8 Michael Warren 8 Carlo Angiuli 4 Anthony Bordg 21 Guillaume Brunerie 22 Chris Kapulkin 23 Egbert Rijke 4 Kristina Sojakova 4 Jeremy Avigad 4 Cyril Cohen 9 Robert Constable 24 Pierre-Louis Curien 11, 12 Peter Dybjer 9 Martín Escardó 25 Kuen-Bang Hou 4 Nicola Gambino 26 Richard Garner 27 Georges Gonthier 28 Thomas Hales 4 Robert Harper 4 Martin Hofmann 29 Pieter Hofstra 30 Joachim Koch 31 Nicolai Kraus 32 Nuo Li 33 Zhaohui Luo 34 Michael Nahas 8 Erik Palmgren 35 Emily Riehl 35 Dana Scott 36 Philip Scott 30 Sergei Soloviev 2 
7 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
11 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UPCité - Université Paris Cité, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
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.
Complete list of metadata
Contributor : Yves Bertot Connect in order to contact the contributor
Submitted on : Thursday, January 23, 2014 - 12:56:04 AM
Last modification on : Thursday, December 1, 2022 - 2:02:08 PM


  • 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⟩



Record views