π_n(S^n) in Homotopy Type Theory - Université Côte d'Azur Access content directly
Conference Papers Year : 2013

π_n(S^n) in Homotopy Type Theory

Daniel R. Licata
  • Function : Author

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.

Dates and versions

hal-01322405 , version 1 (27-05-2016)

Identifiers

Cite

Daniel R. 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⟩
71 View
0 Download

Altmetric

Share

Gmail Mastodon Facebook X LinkedIn More