π_n(S^n) in Homotopy Type Theory

Abstract : Homotopy type theory [Awodey and Warren, 2009; Voevodsky, 2011] is an extension of Martin-Löf’s intensional type theory [Martin-Löf, 1975; Nordström et al., 1990] with new principles such as Voevodsky’s univalence axiom and higher-dimensional inductive types [Lumsdaine and Shulman, 2013]. These extensions are interesting both from a computer science perspective, where they imbue the equality apparatus of type theory with new computational meaning, and from a mathematical perspective, where they allow higher-dimensional mathematics to be expressed cleanly and elegantly in type theory.
Type de document :
Communication dans un congrès
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. 〈10.1007/978-3-319-03545-1_1〉
Liste complète des métadonnées

https://hal.univ-cotedazur.fr/hal-01322405
Contributeur : Guillaume Brunerie <>
Soumis le : vendredi 27 mai 2016 - 10:30:48
Dernière modification le : jeudi 3 mai 2018 - 13:32:58

Identifiants

Collections

Citation

Daniel Licata, Guillaume Brunerie. π_n(S^n) in Homotopy Type Theory. Certified Programs and Proofs, Dec 2013, Melbourne, Australia. 〈10.1007/978-3-319-03545-1_1〉. 〈hal-01322405〉

Partager

Métriques

Consultations de la notice

80