6.1 Introduction
Like the general inductive types we discussed in http://planetmath.org/node/87578Chapter 5, higher inductive types are a general schema for defining new types generated by some constructors. But unlike ordinary inductive types, in defining a higher inductive type we may have βconstructorsβ which generate not only points of that type, but also paths and higher paths in that type. For instance, we can consider the higher inductive type ${\mathrm{\pi \x9d\x95\x8a}}^{1}$ generated by

β’
A point $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}:{\mathrm{\pi \x9d\x95\x8a}}^{1}$, and

β’
A path $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}:\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}{=}_{{\mathrm{\pi \x9d\x95\x8a}}^{1}}\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$.
This should be regarded as entirely analogous to the definition of, for instance, $\mathrm{\pi \x9d\x9f\x90}$, as being generated by

β’
A point ${0}_{\mathrm{\pi \x9d\x9f\x90}}:\mathrm{\pi \x9d\x9f\x90}$ and

β’
A point ${1}_{\mathrm{\pi \x9d\x9f\x90}}:\mathrm{\pi \x9d\x9f\x90}$,
or the definition of $\mathrm{\beta \x84\x95}$ as generated by

β’
A point $0:\mathrm{\beta \x84\x95}$ and

β’
A function $\mathrm{\pi \x9d\x97\x8c\pi \x9d\x97\x8e\pi \x9d\x96\u038c\pi \x9d\x96\u038c}:\mathrm{\beta \x84\x95}\beta \x86\x92\mathrm{\beta \x84\x95}$.
When we think of types as higher groupoids^{}, the more general notion of βgenerationβ is very natural: since a higher groupoid is a βmultisorted objectβ with paths and higher paths as well as points, we should allow βgenerators^{}β in all dimensions^{}.
We will refer to the ordinary sort of constructors (such as $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$) as point constructors or ordinary constructors, and to the others (such as $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$) as path constructors or higher constructors. Each path constructor must specify the starting and ending point of the path, which we call its source and target; for $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$, both source and target are $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$.
Note that a path constructor such as $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$ generates a new inhabitant of an identity type, which is not (at least, not a priori) equal to any previously existing such inhabitant. In particular, $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$ is not a priori equal to ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}}$ (although proving that they are definitely unequal takes a little thought; see Lemma 6.4.1 (http://planetmath.org/64circlesandspheres#Thmprelem1)). This is what distinguishes ${\mathrm{\pi \x9d\x95\x8a}}^{1}$ from the ordinary inductive type $\mathrm{\pi \x9d\x9f\x8f}$.
There are some important points to be made regarding this generalization^{}.
First of all, the word βgenerationβ should be taken seriously, in the same sense that a group can be freely generated by some set. In particular, because a higher groupoid comes with operations^{} on paths and higher paths, when such an object is βgeneratedβ by certain constructors, the operations create more paths that do not come directly from the constructors themselves. For instance, in the higher inductive type ${\mathrm{\pi \x9d\x95\x8a}}^{1}$, the constructor $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$ is not the only nontrivial path from $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$ to $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$; we have also β$\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}\beta \x81\u2019\text{centerdot}\beta \x81\u2019\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$β and β$\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}\beta \x81\u2019\text{centerdot}\beta \x81\u2019\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}\beta \x81\u2019\text{centerdot}\beta \x81\u2019\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$β and so on, as well as ${\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}}^{1}$, etc., all of which are different. This may seem so obvious as to be not worth mentioning, but it is a departure from the behavior of βordinaryβ inductive types, where one can expect to see nothing in the inductive type except what was βput inβ directly by the constructors.
Secondly, this generation is really free generation: higher inductive types do not technically allow us to impose βaxiomsβ, such as forcing^{} β$\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}\beta \x81\u2019\text{centerdot}\beta \x81\u2019\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$β to equal ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}}$. However, in the world of $\mathrm{\beta \x88\x9e}$groupoids, there is little difference^{} between βfree generationβ and βpresentation^{}β, since we can make two paths equal up to homotopy^{} by adding a new 2dimensional generator relating them (e.g.Β a path $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}\beta \x81\u2019\text{centerdot}\beta \x81\u2019\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}={\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}}$ in $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}=\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$). We do then, of course, have to worry about whether this new generator should satisfy its own βaxiomsβ, and so on, but in principle any βpresentationβ can be transformed into a βfreeβ one by making axioms into constructors. As we will see, by adding βtruncation constructorsβ we can use higher inductive types to express classical notions such as group presentations as well.
Thirdly, even though a higher inductive type contains βconstructorsβ which generate paths in that type, it is still an inductive definition of a single type. In particular, as we will see, it is the higher inductive type itself which is given a universal property^{} (expressed, as usual, by an induction^{} principle), and not its identity types. The identity type of a higher inductive type retains the usual induction principle of any identity type (i.e.Β path induction), and does not acquire any new induction principle.
Thus, it may be nontrivial to identify the identity types of a higher inductive type in a concrete way, in contrast to how in http://planetmath.org/node/87569Chapter 2 we were able to give explicit descriptions of the behavior of identity types under all the traditional type forming operations. For instance, are there any paths from $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$ to $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$ in ${\mathrm{\pi \x9d\x95\x8a}}^{1}$ which are not simply composites of copies of $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$ and its inverse^{}? Intuitively, it seems that the answer should be no (and it is), but proving this is not trivial. Indeed, such questions bring us rapidly to problems such as calculating the homotopy groups of spheres, a longstanding problem in algebraic topology for which no simple formula^{} is known. Homotopy type theory brings a new and powerful viewpoint to bear on such questions, but it also requires type theory^{} to become as complex as the answers to these questions.
Fourthly, the βdimensionβ of the constructors (i.e.Β whether they output points, paths, paths between paths, etc.)Β does not have a direct connection to which dimensions the resulting type has nontrivial homotopy in. As a simple example, if an inductive type $B$ has a constructor of type $A\beta \x86\x92B$, then any paths and higher paths in $A$ result in paths and higher paths in $B$, even though the constructor is not a βhigherβ constructor at all. The same thing happens with higher constructors too: having a constructor of type $A\beta \x86\x92(x{=}_{B}y)$ means not only that points of $A$ yield paths from $x$ to $y$ in $B$, but that paths in $A$ yield paths between these paths, and so on. As we will see, this possibility is responsible for much of the power of higher inductive types.
On the other hand, it is even possible for constructors without higher types in their inputs to generate βunexpectedβ higher paths. For instance, in the 2dimensional sphere ${\mathrm{\pi \x9d\x95\x8a}}^{2}$ generated by

β’
A point $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}:{\mathrm{\pi \x9d\x95\x8a}}^{2}$, and

β’
A 2dimensional path $\mathrm{\pi \x9d\x97\x8c\pi \x9d\x97\x8e\pi \x9d\x97\x8b\pi \x9d\x96\u038f}:{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}}={\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}}$ in $\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}=\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}$,
there is a nontrivial 3dimensional path from ${\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{{\mathrm{\pi \x9d\x97\x8b\pi \x9d\x96\u038e\pi \x9d\x96\u038f\pi \x9d\x97\x85}}_{\mathrm{\pi \x9d\x96\xbb\pi \x9d\x96\u038a\pi \x9d\x97\x8c\pi \x9d\x96\u038e}}}$ to itself. Topologists will recognize this path as an incarnation of the Hopf fibration. From a categorytheoretic point of view, this is the same sort of phenomenon as the fact mentioned above that ${\mathrm{\pi \x9d\x95\x8a}}^{1}$ contains not only $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$ but also $\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}\beta \x81\u2019\text{centerdot}\beta \x81\u2019\mathrm{\pi \x9d\x97\x85\pi \x9d\x97\x88\pi \x9d\x97\x88\pi \x9d\x97\x89}$ and so on: itβs just that in a higher groupoid, there are operations which raise dimension. Indeed, we saw many of these operations back in Β§2.1 (http://planetmath.org/21typesarehighergroupoids): the associativity and unit laws are not just properties, but operations, whose inputs are 1paths and whose outputs are 2paths.
Title  6.1 Introduction 

\metatable 