π_n(S~n) in Homotopy Type Theory

摘要

Homotopy type theory [Awodey and Warren, 2009; Voevodsky, 2011] is an extension of Martin-Loef's intensional type theory [Martin-Loef, 1975; Nordstroem 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. One example of higher-dimensional mathematics is the subject of homotopy theory, a branch of algebraic topology.