Higher inductive types


One of the classical advantages of type theoryPlanetmathPlanetmath is its simple and effective techniques for working with inductively defined structuresMathworldPlanetmath. The simplest nontrivial inductively defined structure is the natural numbersMathworldPlanetmath, which is inductively generated by zero and the successor function. From this statement one can algorithmically extract the principle of mathematical induction, which characterizes the natural numbers. More general inductive definitions encompass lists and well-founded trees of all sorts, each of which is characterized by a corresponding “inductionMathworldPlanetmath principle”. This includes most data structures used in certain programming languages; hence the usefulness of type theory in formal reasoning about the latter. If conceived in a very general sense, inductive definitions also include examples such as a disjoint unionMathworldPlanetmath A+B, which may be regarded as “inductively” generated by the two injections AA+B and BA+B. The “induction principle” in this case is “proof by case analysis”, which characterizes the disjoint union.

In homotopy theory, it is natural to consider also “inductively defined spaces” which are generated not merely by a collectionMathworldPlanetmath of points, but also by collections of paths and higher paths. Classically, such spaces are called CW complexes. For instance, the circle S1 is generated by a single point and a single path from that point to itself. Similarly, the 2-sphere S2 is generated by a single point b and a single two-dimensional path from the constant path at b to itself, while the torus T2 is generated by a single point, two paths p and q from that point to itself, and a two-dimensional path from p\centerdotq to q\centerdotp.

By using the identification of paths with identitiesPlanetmathPlanetmathPlanetmath in homotopy type theory, these sort of “inductively defined spaces” can be characterized in type theory by “induction principles”, entirely analogously to classical examples such as the natural numbers and the disjoint union. The resulting higher inductive types give a direct “logical” way to reason about familiar spaces such as spheres, which (in combination with univalence) can be used to perform familiar arguments from homotopy theory, such as calculating homotopy groups of spheres, in a purely formal way. The resulting proofs are a marriage of classical homotopy-theoretic ideas with classical type-theoretic ones, yielding new insight into both disciplines.

Moreover, this is only the tip of the iceberg: many abstract constructions from homotopy theory, such as homotopy colimits, suspensions, Postnikov towers, localizationMathworldPlanetmath, completion, and spectrification, can also be expressed as higher inductive types. Many of these are classically constructed using Quillen’s “small object argument”, which can be regarded as a finite way of algorithmically describing an infiniteMathworldPlanetmath CW complex presentationMathworldPlanetmathPlanetmath of a space, just as “zero and successorMathworldPlanetmathPlanetmathPlanetmath” is a finite algorithmic description of the infinite set of natural numbers. Spaces produced by the small object argument are infamously complicated and difficult to understand; the type-theoretic approach is potentially much simpler, bypassing the need for any explicit construction by giving direct access to the appropriate “induction principle”. Thus, the combination of univalence and higher inductive types suggests the possibility of a revolution, of sorts, in the practice of homotopy theory.

Title Higher inductive types
\metatable