Skip to Main content Skip to Navigation
Conference papers

π_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.
Complete list of metadatas
Contributor : Guillaume Brunerie <>
Submitted on : Friday, May 27, 2016 - 10:30:48 AM
Last modification on : Monday, October 12, 2020 - 2:28:06 PM

Links full text




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⟩



Record views