6.13 The general syntax of higher inductive definitions

In §5.6 (http://planetmath.org/56thegeneralsyntaxofinductivedefinitions), we discussed the conditions on a putative “inductive definition” which make it acceptable, namely that all inductive occurrences of the type in its constructors are “strictly positive”. In this section, we say something about the additional conditions required for higher inductive definitions. Finding a general syntactic description of valid higher inductive definitions is an area of current research, and all of the solutions proposed to date are somewhat technical in nature; thus we only give a general description and not a precise definition. Fortunately, the corner cases never seem to arise in practice.

Like an ordinary inductive definition, a higher inductive definition is specified by a list of constructors, each of which is a (dependent) function. For simplicity, we may require the inputs of each constructor to satisfy the same condition as the inputs for constructors of ordinary inductive types. In particular, they may contain the type being defined only strictly positively. Note that this excludes definitions such as the $0$ -truncation as presented in §6.9 (http://planetmath.org/69truncations), where the input of a constructor contains not only the inductive type being defined, but its identity type as well. It may be possible to extend the syntax to allow such definitions; but also, in §7.3 (http://planetmath.org/73truncations) we will give a different construction of the $0$ -truncation whose constructors do satisfy the more restrictive condition.

The only difference between an ordinary inductive definition and a higher one, then, is that the output type of a constructor may be, not the type being defined ( $W$ , say), but some identity type of it, such as $u=_{W}v$ , or more generally an iterated identity type such as $p=_{({u=_{W}v})}q$ . Thus, when we give a higher inductive definition, we have to specify not only the inputs of each constructor, but the expressions $u$ and $v$ (or $u$ , $v$ , $p$ , and $q$ , etc.) which determine the source and target of the path being constructed.

Importantly, these expressions may refer to other constructors of $W$ . For instance, in the definition of $\mathbb{S}^{1}$ , the constructor $\mathsf{loop}$ has both $u$ and $v$ being $\mathsf{base}$ , the previous constructor. To make sense of this, we require the constructors of a higher inductive type to be specified in order, and we allow the source and target expressions $u$ and $v$ of each constructor to refer to previous constructors, but not later ones. (Of course, in practice the constructors of any inductive definition are written down in some order, but for ordinary inductive types that order is irrelevant.)

Note that this order is not necessarily the order of “dimension”: in principle, a 1-dimensional path constructor could refer to a 2-dimensional one and hence need to come after it. However, we have not given the 0-dimensional constructors (point constructors) any way to refer to previous constructors, so they might as well all come first. And if we use the hub-and-spoke construction (§6.7 (http://planetmath.org/67hubsandspokes)) to reduce all constructors to points and 1-paths, then we might assume that all point constructors come first, followed by all 1-path constructors — but the order among the 1-path constructors continues to matter.

The remaining question is, what sort of expressions can $u$ and $v$ be? We might hope that they could be any expression at all involving the previous constructors. However, the following example shows that a naive approach to this idea does not work.

Example 6.13.1.

Consider a family of functions $f:\mathchoice{\prod_{X:\mathcal{U}}\,}{\mathchoice{{\textstyle\prod_{(X:% \mathcal{U})}}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(X:\mathcal{U})}}}{\prod_{(X:% \mathcal{U})}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:\mathcal{U})}}}{\mathchoice{% {\textstyle\prod_{(X:\mathcal{U})}}}{\prod_{(X:\mathcal{U})}}{\prod_{(X:% \mathcal{U})}}{\prod_{(X:\mathcal{U})}}}(X\to X)$ . Of course, $f_{X}$ might be just $\mathsf{id}_{X}$ for all $X$ , but other such $f$ s may also exist. For instance, nothing prevents $f_{\mathbf{2}}:\mathbf{2}\to\mathbf{2}$ from being the nonidentity automorphism (see http://planetmath.org/node/87835Exercise 6.9).

Now suppose that we attempt to define a higher inductive type $K$ generated by:

•

two elements $a, b : K$ , and
•

a path $\sigma:f_{K}(a)=f_{K}(b)$ .

What would the induction principle for $K$ say? We would assume a type family $P:K\to\mathcal{U}$ , and of course we would need $x:P(a)$ and $y:P(b)$ . The remaining datum should be a dependent path in $P$ living over $\sigma$ , which must therefore connect some element of $P(f_{K}(a))$ to some element of $P(f_{K}(b))$ . But what could these elements possibly be? We know that $P(a)$ and $P(b)$ are inhabited by $x$ and $y$ , respectively, but this tells us nothing about $P(f_{K}(a))$ and $P(f_{K}(b))$ .

Clearly some condition on $u$ and $v$ is required in order for the definition to be sensible. It seems that, just as the domain of each constructor is required to be (among other things) a covariant functor, the appropriate condition on the expressions $u$ and $v$ is that they define natural transformations. Making precise sense of this requirement is beyond the scope of this book, but informally it means that $u$ and $v$ must only involve operations which are preserved by all functions between types.

For instance, it is permissible for $u$ and $v$ to refer to concatenation of paths, as in the case of the final constructor of the torus in §6.6 (http://planetmath.org/66cellcomplexes), since all functions in type theory preserve path concatenation (up to homotopy). However, it is not permissible for them to refer to an operation like the function $f$ in Example 6.13.1 (http://planetmath.org/613thegeneralsyntaxofhigherinductivedefinitions#Thmpreeg1), which is not necessarily natural: there might be some function $g:X\to Y$ such that $f_{Y}\circ g\neq g\circ f_{X}$ . (Univalence implies that $f_{X}$ must be natural with respect to all equivalences, but not necessarily with respect to functions that are not equivalences.)

The intuition of naturality supplies only a rough guide for when a higher inductive definition is permissible. Even if it were possible to give a precise specification of permissible forms of such definitions in this book, such a specification would probably be out of date quickly, as new extensions to the theory are constantly being explored. For instance, the presentation of $n$ -spheres in terms of “dependent $n$ -loops” referred to in §6.4 (http://planetmath.org/64circlesandspheres), and the “higher inductive-recursive definitions” used in http://planetmath.org/node/87585Chapter 11, were innovations introduced while this book was being written. We encourage the reader to experiment — with caution.

Title	6.13 The general syntax of higher inductive definitions
\metatable