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 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
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
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

https://hal.inria.fr/hal-00935057
Contributeur : Yves Bertot <>
Soumis le : jeudi 23 janvier 2014 - 00:56:04
Dernière modification le : mercredi 12 juillet 2017 - 01:17:16

Identifiants

  • HAL Id : hal-00935057, version 1

Citation

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>

Partager

Métriques

Consultations de la notice

1178