6.2 Induction principles and dependent paths

When we describe a higher inductive type such as the circle as being generated by certain constructors, we have to explain what this means by giving rules analogous to those for the basic type constructors from http://planetmath.org/node/87533Chapter 1. The constructors themselves give the introduction rules, but it requires a bit more thought to explain the elimination rules, i.e. the induction and recursion principles. In this book we do not attempt to give a general formulation of what constitutes a “higher inductive definition” and how to extract the elimination rule from such a definition — indeed, this is a subtle question and the subject of current research. Instead we will rely on some general informal discussion and numerous examples.

The recursion principle is usually easy to describe: given any type equipped with the same structure with which the constructors equip the higher inductive type in question, there is a function which maps the constructors to that structure. For instance, in the case of $\mathbb{S}^{1}$ , the recursion principle says that given any type $B$ equipped with a point $b : B$ and a path $\ell:b=b$ , there is a function $f:\mathbb{S}^{1}\to B$ such that $f(\mathsf{base})=b$ and $\mathsf{ap}_{f}(\mathsf{loop})=\ell$ .

The latter two equalities are the computation rules. There is, however, a question of whether these computation rules are judgmental equalities or propositional equalities (paths). For ordinary inductive types, we had no qualms about making them judgmental, although we saw in http://planetmath.org/node/87578Chapter 5 that making them propositional would still yield the same type up to equivalence. In the ordinary case, one may argue that the computation rules are really definitional equalities, in the intuitive sense described in the Introduction.

For higher inductive types, this is less clear. Moreover, since the operation $\mathsf{ap}_{f}$ is not really a fundamental part of the type theory, but something that we defined using the induction principle of identity types (and which we might have defined in some other, equivalent, way), it seems inappropriate to refer to it explicitly in a judgmental equality. Judgmental equalities are part of the deductive system, which should not depend on particular choices of definitions that we may make within that system. There are also semantic and implementation issues to consider; see the Notes (http://planetmath.org/chapter6notes).

It does seem unproblematic to make the computational rules for the point constructors of a higher inductive type judgmental. In the example above, this means we have $f(\mathsf{base})\equiv b$ , judgmentally. This choice facilitates a computational view of higher inductive types. Moreover, it also greatly simplifies our lives, since otherwise the second computation rule $\mathsf{ap}_{f}(\mathsf{loop})=\ell$ would not even be well-typed as a propositional equality; we would have to compose one side or the other with the specified identification of $f(\mathsf{base})$ with $b$ . (Such problems do arise eventually, of course, when we come to talk about paths of higher dimension, but that will not be of great concern to us here. See also §6.7 (http://planetmath.org/67hubsandspokes).) Thus, we take the computation rules for point constructors to be judgmental, and those for paths and higher paths to be propositional.¹¹In particular, in the language of §1.1 (http://planetmath.org/11typetheoryversussettheory), this means that our higher inductive types are a mix of rules (specifying how we can introduce such types and their elements, their induction principle, and their computation rules for point constructors) and axioms (the computation rules for path constructors, which assert that certain identity types are inhabited by otherwise unspecified terms). We may hope that eventually, there will be a better type theory in which higher inductive types, like univalence, will be presented using only rules and no axioms.

Remark 6.2.1.

Recall that for ordinary inductive types, we regard the computation rules for a recursively defined function as not merely judgmental equalities, but definitional ones, and thus we may use the notation $:\!\!\equiv$ for them. For instance, the truncated predecessor function $p:\mathbb{N}\to\mathbb{N}$ is defined by $p(0):\!\!\equiv 0$ and $p(\mathsf{succ}(n)):\!\!\equiv n$ . In the case of higher inductive types, this sort of notation is reasonable for the point constructors (e.g. $f(\mathsf{base}):\!\!\equiv b$ ), but for the path constructors it could be misleading, since equalities such as ${f}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}=\ell$ are not judgmental. Thus, we hybridize the notations, writing instead ${f}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}:=\ell$ for this sort of “propositional equality by definition”.

Now, what about the induction principle (the dependent eliminator)? Recall that for an ordinary inductive type $W$ , to prove by induction that $\mathchoice{\prod_{x:W}\,}{\mathchoice{{\textstyle\prod_{(x:W)}}}{\prod_{(x:W)% }}{\prod_{(x:W)}}{\prod_{(x:W)}}}{\mathchoice{{\textstyle\prod_{(x:W)}}}{\prod% _{(x:W)}}{\prod_{(x:W)}}{\prod_{(x:W)}}}{\mathchoice{{\textstyle\prod_{(x:W)}}% }{\prod_{(x:W)}}{\prod_{(x:W)}}{\prod_{(x:W)}}}P(x)$ , we must specify, for each constructor of $W$ , an operation on $P$ which acts on the “fibers” above that constructor in $W$ . For instance, if $W$ is the natural numbers $\mathbb{N}$ , then to prove by induction that $\mathchoice{\prod_{x:\mathbb{N}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbb{N% })}}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}}% {\mathchoice{{\textstyle\prod_{(x:\mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{\prod% _{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{N})}}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:\mathbb{N})}}{\prod_{(x:% \mathbb{N})}}}P(x)$ , we must specify

•

An element $b:P(0)$ in the fiber over the constructor $0:\mathbb{N}$ , and
•

For each $n:\mathbb{N}$ , a function $P(n)\to P(\mathsf{succ}(n))$ .

The second can be viewed as a function “ $P\to P$ ” lying over the constructor $\mathsf{succ}:\mathbb{N}\to\mathbb{N}$ , generalizing how $b:P(0)$ lies over the constructor $0:\mathbb{N}$ .

By analogy, therefore, to prove that $\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}P(x)$ , we should specify

•

An element $b:P(\mathsf{base})$ in the fiber over the constructor $\mathsf{base}:\mathbb{S}^{1}$ , and
•

A path from $b$ to $b$ “lying over the constructor $\mathsf{loop}:\mathsf{base}=\mathsf{base}$ ”.

Note that even though $\mathbb{S}^{1}$ contains paths other than $\mathsf{loop}$ (such as $\mathsf{refl}_{\mathsf{base}}$ and $\mathsf{loop}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}% }}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathsf{loop}$ ), we only need to specify a path lying over the constructor itself. This expresses the intuition that $\mathbb{S}^{1}$ is “freely generated” by its constructors.

The question, however, is what it means to have a path “lying over” another path. It definitely does not mean simply a path $b=b$ , since that would be a path in the fiber $P(\mathsf{base})$ (topologically, a path lying over the constant path at $\mathsf{base}$ ). Actually, however, we have already answered this question in http://planetmath.org/node/87569Chapter 2: in the discussion preceding Lemma 2.3.4 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem3) we concluded that a path from $u:P(x)$ to $v:P(y)$ lying over $p:x=y$ can be represented by a path ${p}_{*}\mathopen{}\left({u}\right)\mathclose{}=v$ in the fiber $P(y)$ . Since we will have a lot of use for such dependent paths in this chapter, we introduce a special notation for them:

(u=^{P}_{p}v):\!\!\equiv(\mathsf{transport}^{P}(p,u)=v).

(6.2.2)

Remark 6.2.3.

There are other possible ways to define dependent paths. For instance, instead of ${p}_{*}\mathopen{}\left({u}\right)\mathclose{}=v$ we could consider $u={(\mathord{{p}^{-1}})}_{*}\mathopen{}\left({v}\right)\mathclose{}$ . We could also obtain it as a special case of a more general “heterogeneous equality”, or with a direct definition as an inductive type family. All these definitions result in equivalent types, so in that sense it doesn’t much matter which we pick. However, choosing ${p}_{*}\mathopen{}\left({u}\right)\mathclose{}=v$ as the definition makes it easiest to conclude other things about dependent paths, such as the fact that $\mathsf{apd}_{f}$ produces them, or that we can compute them in particular type families using the transport lemmas in §2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers).

With the notion of dependent paths in hand, we can now state more precisely the induction principle for $\mathbb{S}^{1}$ : given $P:\mathbb{S}^{1}\to\mathcal{U}$ and

•

An element $b:P(\mathsf{base})$ , and
•

A path $\ell:b=^{P}_{\mathsf{loop}}b$ ,

there is a function $f:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}P(x)$ such that $f(\mathsf{base})\equiv b$ and $\mathsf{apd}_{f}\mathopen{}\left(\mathsf{loop}\right)\mathclose{}=\ell$ . As in the non-dependent case, we speak of defining $f$ by $f(\mathsf{base}):\!\!\equiv b$ and $\mathsf{apd}_{f}\mathopen{}\left(\mathsf{loop}\right)\mathclose{}:=\ell$ .

Remark 6.2.4.

When describing an application of this induction principle informally, we regard it as a splitting of the goal “ $P(x)$ for all $x:\mathbb{S}^{1}$ ” into two cases, which we will sometimes introduce with phrases such as “when $x$ is $\mathsf{base}$ ” and “when $x$ varies along $\mathsf{loop}$ ”, respectively. There is no specific mathematical meaning assigned to “varying along a path”: it is just a convenient way to indicate the beginning of the corresponding section of a proof; see Lemma 6.4.2 (http://planetmath.org/64circlesandspheres#Thmprelem2) for an example.

Topologically, the induction principle for $\mathbb{S}^{1}$ can be visualized as shown in Figure 6.1 (http://planetmath.org/62inductionprinciplesanddependentpaths#S0.F1). Given a fibration over the circle (which in the picture is a torus), to define a section of this fibration is the same as to give a point $b$ in the fiber over $\mathsf{base}$ along with a path from $b$ to $b$ lying over $\mathsf{loop}$ . The way we interpret this type-theoretically, using our definition of dependent paths, is shown in Figure 6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths#S0.F2): the path from $b$ to $b$ over $\mathsf{loop}$ is represented by a path from ${\mathsf{loop}}_{*}\mathopen{}\left({b}\right)\mathclose{}$ to $b$ in the fiber over $\mathsf{base}$ .

\includegraphics

HoTT_fig_6.2.1.png

Figure 6.1: The topological induction principle for

\mathbb{S}^{1}

\includegraphics

HoTT_fig_6.2.2.png

Figure 6.2: The type-theoretic induction principle for

\mathbb{S}^{1}

Of course, we expect to be able to prove the recursion principle from the induction principle, by taking $P$ to be a constant type family. This is in fact the case, although deriving the non-dependent computation rule for $\mathsf{loop}$ (which refers to $\mathsf{ap}_{f}$ ) from the dependent one (which refers to $\mathsf{apd}_{f}$ ) is surprisingly a little tricky.

Lemma 6.2.5.

If $A$ is a type together with $a : A$ and $p:a=_{A}a$ , then there is a function $f:\mathbb{S}^{1}\to{}A$ with

	$\displaystyle f(\mathsf{base})$	$\displaystyle:\!\!\equiv a$
	$\displaystyle\mathsf{ap}_{f}(\mathsf{loop})$	$\displaystyle:=p.$

Proof.

We would like to apply the induction principle of $\mathbb{S}^{1}$ to the constant type family, $({\lambda}x.\,A):\mathbb{S}^{1}\to\mathcal{U}$ . The required hypotheses for this are a point of $({\lambda}x.\,A)(\mathsf{base})\equiv A$ , which we have (namely $a : A$ ), and a dependent path in $a=^{x\mapsto A}_{\mathsf{loop}}a$ , or equivalently $\mathsf{transport}^{x\mapsto A}(\mathsf{loop},a)=a$ . This latter type is not the same as the type $a=_{A}a$ where $p$ lives, but it is equivalent to it, because by Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem4) we have $\mathsf{transportconst}^{A}_{\mathsf{loop}}(a):\mathsf{transport}^{x\mapsto A}% (\mathsf{loop},a)=a$ . Thus, given $a : A$ and $p:a=a$ , we can consider the composite

\mathsf{transportconst}^{A}_{\mathsf{loop}}(a)\mathchoice{\mathbin{\raisebox{2% .15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}% {\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p:(a=^{x\mapsto A}_{% \mathsf{loop}}a).

Applying the induction principle, we obtain $f:\mathbb{S}^{1}\to A$ such that

	$\displaystyle f(\mathsf{base})$	$\displaystyle\equiv a\qquad\text{and}$		(6.2.6)
	$\displaystyle\mathsf{apd}_{f}(\mathsf{loop})$	$\displaystyle=\mathsf{transportconst}^{A}_{\mathsf{loop}}(a)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p.$		(6.2.6)

It remains to derive the equality $\mathsf{ap}_{f}(\mathsf{loop})=p$ . However, by Lemma 2.3.8 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem5), we have

\mathsf{apd}_{f}(\mathsf{loop})=\mathsf{transportconst}^{A}_{\mathsf{loop}}(f(% \mathsf{base}))\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot% $}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathsf{ap}_{f}(\mathsf{loop}).

Combining this with (6.2.6) and canceling the occurrences of $\mathsf{transportconst}$ (which are the same by (6.2.6)), we obtain $\mathsf{ap}_{f}(\mathsf{loop})=p$ . ∎

We also have a corresponding uniqueness principle.

Lemma 6.2.6.

If $A$ is a type and $f,g:\mathbb{S}^{1}\to{}A$ are two maps together with two equalities $p, q$ :

	$\displaystyle p:f(\mathsf{base})$	$\displaystyle=_{A}g(\mathsf{base}),$
	$\displaystyle q:{f}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}$	$\displaystyle=^{{\lambda}x.\,x=_{A}x}_{p}{g}\mathopen{}\left({\mathsf{loop}}% \right)\mathclose{}.$

Then for all $x:\mathbb{S}^{1}$ we have $f(x)=g(x)$ .

Proof.

This is just the induction principle for the type family $P(x):\!\!\equiv(f(x)=g(x))$ . ∎

These two lemmas imply the expected universal property of the circle:

Lemma 6.2.7.

For any type $A$ we have a natural equivalence

(\mathbb{S}^{1}\to A)\;\simeq\;\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}(x=x).

Proof.

We have a canonical function $f:(\mathbb{S}^{1}\to A)\to\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}(x=x)$ defined by $f(g):\!\!\equiv(g(\mathsf{base}),{g}\mathopen{}\left({\mathsf{loop}}\right)% \mathclose{})$ . The induction principle shows that the fibers of $f$ are inhabited, while the uniqueness principle shows that they are mere propositions. Hence they are contractible, so $f$ is an equivalence. ∎

As in §5.5 (http://planetmath.org/55homotopyinductivetypes), we can show that the conclusion of Lemma 6.2.7 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprelem3) is equivalent to having an induction principle with propositional computation rules. Other higher inductive types also satisfy lemmas analogous to Lemma 6.2.5 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprelem1),Lemma 6.2.7 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprelem3); we will generally leave their proofs to the reader. We now proceed to consider many examples.

Title	6.2 Induction principles and dependent paths
\metatable