Chapter 6 Notes

The general idea of higher inductive types was conceived in discussions between Andrej Bauer, Peter Lumsdaine, Mike Shulman, and Michael Warren at the Oberwolfach meeting in 2011, although there are some suggestions of some special cases in earlier work. Subsequently, Guillaume Brunerie and Dan Licata contributed substantially to the general theory, especially by finding convenient ways to represent them in computer proof assistants and do homotopy theory with them (see http://planetmath.org/node/87582Chapter 8).

A general discussion of the syntax of higher inductive types, and their semantics in higher-categorical models, appears in [8]. As with ordinary inductive types, models of higher inductive types can be constructed by transfinite iterative processes; a slogan is that ordinary inductive types describe free monads while higher inductive types describe presentations of monads.The introduction of path constructors also involves the model-category-theoretic equivalence between “right homotopies” (defined using path spaces) and “left homotopies” (defined using cylinders) — the fact that this equivalence is generally only up to homotopy provides a semantic reason to prefer propositional computation rules for path constructors.

Another (temporary) reason for this preference comes from the limitations of existing computer implementations. Proof assistants like Coq and Agda have ordinary inductive types built in, but not yet higher inductive types. We can of course introduce them by assuming lots of axioms, but this results in only propositional computation rules. However, there is a trick due to Dan Licata which implements higher inductive types using private data types; this yields judgmental rules for point constructors but not path constructors.

The type-theoretic description of higher spheres using loop spaces and suspensions in §6.4 (http://planetmath.org/64circlesandspheres),§6.5 (http://planetmath.org/65suspensions) is largely due to Brunerie and Licata; Hou has given a type-theoretic version of the alternative description that uses $n$-dimensional paths. The reduction of higher paths to 1-dimensional paths with hubs and spokes (§6.7 (http://planetmath.org/67hubsandspokes)) is due to Lumsdaine and Shulman. The description of truncation as a higher inductive type is due to Lumsdaine; the $(-1)$-truncation is closely related to the “bracket types” of [1]. The flattening lemma was first formulated in generality by Brunerie.

Quotient types are unproblematic in extensional type theory, such as NuPRL [5]. They are often added by passing to an extended system of setoids. However, quotients are a trickier issue in intensional type theory (the starting point for homotopy type theory), because one cannot simply add new propositional equalities without specifying how they are to behave. Some solutions to this problem have been studied [7],[3],[2], and several different notions of quotient types have been considered. The construction of set-quotients using higher-inductives provides an argument for our particular approach (which is similar to some that have previously been considered), because it arises as an instance of a general mechanism. Our construction does not yet provide a new solution to all the computational problems related to quotients, since we still lack a good computational understanding of higher inductive types in general—but it does mean that ongoing work on the computational interpretation of higher inductives applies to the quotients as well. The construction of quotients in terms of equivalence classes is, of course, a standard set-theoretic idea, and a well-known aspect of elementary topos theory; its use in type theory (which depends on the univalence axiom, at least for mere propositions) was proposed by Voevodsky. The fact that quotient types in intensional type theory imply function extensionality was proved by [7], inspired by the work of [4] on exact completions; Lemma 6.3.2 (http://planetmath.org/63theinterval#Thmprelem2) is an adaptation of such arguments.

Title	Chapter 6 Notes