Is path induction constructive?

I'm reading through the HoTT book and I have a hard time with path induction.

When I look at the type in the section 1.12.1: $$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}} \left( \left(\prod_{x:A}C(x,x,\text{refl}_x)\right) \to \prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p) \right),$$ I have no issue understanding what that means (I just have written the type from memory, to check that).

What I have issue with is the next very statement:
$$\text{with the equality}\quad \text{ind}_{=_A}(C,c,x,x,\text{refl}_x):\equiv c(x)$$ my first impression was that this last expression does not define the resulting function $$f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$$ but just states its property.

That is in contrast to previous examples of the induction principles $\text{ind}_{A\times B}$,$\text{ind}_{A+B}$ or $\text{ind}_\mathbb{N}$ -- there are defining equations for those elements -- we actually know how to construct the resulting function, given the premises. Which is in agreement with the "constructiveness" of type theory adverted throughout the chapter.

Going back to $\text{ind}_{=_A}$, I was suspicious about the fact that (looks like) it is not defined. Stating that the element $f$ just exists seemed out of tune with the rest of the chapter. And indeed, the section 1.12.1 seems to stress that my impression is wrong and we in fact have defined

... the function $f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$ defined by
path induction from $c:\prod_{x:A}C(x,x,\text{refl}_x)$, which moreover
satisfies $f(x,x,\text{refl}_x):\equiv c(x)$ ...

That leaves me utterly confused, but I have a feeling that this point is very important for all the further developments. So which of the two readings for $\text{ind}_{=_A}$ should I go with? Or, probably, I'm missing some important subtlety and the answer is "neither"?

• By the way, this is not really a HoTT-specific question, but a more general "dependent types" question. – cody Jul 29 '14 at 22:04

It is an illusion that the computation rules "define" or "construct" the objects they speak about. You correctly observed that the equation for $\mathrm{ind}_{=_A}$ does not "define" it, but failed to observe that the same is true in other cases as well. Let us consider the induction principle for the unit type $1$, which seems particularly obviously "determined". According to Section 1.5 of the HoTT book we have $$\mathrm{ind}_1 : \prod_{C : 1 \to \mathtt{Type}} C(\star) \to \prod_{x : 1} P(x)$$ with the equation $$\mathrm{ind}_1 (C, c, \star) = c.$$ Does this "define" or "construct" $\mathrm{ind}_1$ in the sense that it leaves no doubt as to what $\mathrm{ind}_1$ "does"? For instance, set $C(x) = \mathbb{N}$ and $a = 42$, and consider what we could say about $$\mathrm{ind}_1(C, 42, e)$$ for a given expression $e$ of type $1$. Your first thought might be that we can reduce this to $42$ because "$\star$ is the only element of $1$". But to be quite precise, the equation for $\mathrm{ind}_1$ is applicable only if we show $e \equiv \star$, which is impossible when $e$ is a variable, for example. We can try to wiggle out of this and say that we are only interested in computation with closed terms, so $e$ should be closed.

Is it not the case that every closed term $e$ of type $1$ is judgmentally equal to $\star$? That depends on nasty details and complicated proofs of normalization, actually. In the case of HoTT the answer is "no" because $e$ could contain instances of the Univalence Axiom, and it is not clear what do to about that (this is the open problem in HoTT).

We can circumvent the trouble with univalance by considering a version of type theory which does have good properties so that every closed term of type $1$ is judgmentally equal to $\star$. In that case it is fair to say that we do know how to compute with $\mathrm{ind}_1$, but:

1. The same will hold for the identity type, because every closed term of an identity type will be judgmentally equal to some $\mathrm{refl}(a)$, and so then the equation for $\mathrm{ind}_{=_A}$ will tell us how to compute.

2. Just because we know how to compute with closed terms of a type, that does not mean we have actually defined anything because there is more to a type than its closed terms, as I tried to explain once.

For example, Martin-Löf type theory (without the identity types) can be interpreted domain-theoretically in such a way that $1$ contains two elements $\bot$ and $\top$, where $\top$ corresponds to $\star$ and $\bot$ to non-termination. Alas, since there is no way to write down a non-terminating expression in type theory, $\bot$ cannot be named. Consequently, the equation for $\mathrm{ind}_1$ does not tell us how to compute on $\bot$ (the two obvious choices being "eagerly" and "lazily").

In software engineering terms, I would say we have a confusion between specification and implementation. The HoTT axioms for the identity types are a specification. The equation $\mathrm{ind}_{=_C}(C,c,x,x,\mathrm{refl}(x)) \equiv c(x)$ is not telling us how to compute with, or how to construct $\mathrm{ind}_{=_C}$, but rather that however $\mathrm{ind}_{=_C}$ is "implemented", we require that it satisfy the equation. It is a separate question whether such $\mathrm{ind}_{=_C}$ can be obtained in a constructive fashion.

Lastly, I am a bit weary of how you use the word "constructive". It looks as if you think that "constructive" is the same as "defined". Under that interpretation the Halting oracle is constructive, because its behavior is defined by the requirement we impose on it (namely that it output 1 or 0 according to whether the given machine halts). It is prefectly possible to describe objects which only exist in a non-constructive setting. Conversely, it is perfectly possible to speak constructively about properties and other things that cannot actually be computed. Here is one: the relation $H \subseteq \mathbb{N} \times \{0,1\}$ defined by $$H(n,d) \iff (d = 1 \Rightarrow \text{n-th machine halts}) \land (d = 0 \Rightarrow \text{n-th machine diverges})$$ is constructive, i.e., there is nothing wrong with this definition from a constructive point of view. It just so happens that constructively one cannot show that $H$ is a total relation, and its characteristic map $\chi_H : \mathbb{N} \times \{0,1\} \to \mathsf{Prop}$ does not factor through $\mathtt{bool}$, so we cannot "compute" its values.

Addendum: The title of your question is "Is path induction constructive?" After having cleared up the difference between "constructive" and "defined", we can answer the question. Yes, path induction is known to be constructive in certain cases:

1. If we restrict to type theory without Univalence so that we can show strong normalization, then path induction and everything else is constructive because there are algorithms that perform the normalization procedure.

2. There are realizability models of type theory, which explain how every closed term in type theory corresponds to a Turing machine. However, these models satisfy Streicher's Axiom K, which rules out Univalence.

3. There is a translation of type theory (again without Univalence) into constructive set theory CZF. Once again, this validates Streicher's axiom K.

4. There is a groupoid model inside realizability models which allows us to interpret type theory without Streicher's K. This is preliminary work by Steve Awodey and myself.

We really need to sort out the constructive status of Univalence.

I'm no HoTT person, but I'll throw in my two-cents.

Suppose we are wanting to make a function $$f_A : \prod_{x,y : A}\prod_{p : x =_A y} C(x,y,p)$$ How would we do this? Well, suppose we're given any $x,y : A$ and a proof of their equality $p : x =_A y$. Since I know nothing about the arbitrary type $A$, I know nothing about the structure' of $x,y$. However, I know something about the specific equality type: it has a single constructor, $$\mathsf{refl}_a : a =_A a, \text{ for any } a : A$$ Hence, $p \equiv \mathsf{refl}_a$ for some $a : A$, but this would force $x=a=y$. Hence, if we had an element of $C(x,x,\mathsf{refl}_x)$ for any $x : A$; ie if we had a function $$base_C : \prod_{x:A}C(x,x,\mathsf{refl}_x)$$ (for our specific $C$), then our function $f_A$ can be defined as follows: $$f_A(x,y,p) := base_C(x,x,p)$$.

Getting rid of the subscripts leads to the general inductive definition.

Hope that helps!

PS. I'm no HoTT guy, so I'm assuming Axiom K'. More precisely, I'm assuming that an element $e$ of type $E$ must be the result of repeated applications of constructor of $E$. As far as I know, HoTT, probably chapter 2 onwards, throws away this notion ... and that makes absolutely no sense to me.

• Perhaps you can make some sense of it, or at least get worried about your current intuitions by checking out math.andrej.com/2013/08/28/the-elements-of-an-inductive-type where I try to explain why it is harmful to think that the closed terms of a type are all there is to a type. – Andrej Bauer Jul 30 '14 at 14:34
• By the way, you need not asssume Axiom K. For your answer to make sense, you need to know that every closed term of an identity type normalizes to $\mathsf{refl}$. This has nothing to do with Axiom K, as such a normalization property does not prove axiom K, nor does it follow from axiom K. – Andrej Bauer Jul 30 '14 at 14:52

The problem you are talking about is relevant not to HoTT itself, but rather to the construction of HoTT models. When we construct a model of HoTT in some category we have to choose a morphism for each functional constant that we defined, so that all stated relations hold. This choice is inherently non-unique, and this non-uniqueness of model (even within the same category) cannot be described inside HoTT itself. In some cases (with extra knowledge) we can prove that the results of our computations do not essentially depend on the chosen interpretations. For example, if you choose another $$\mathrm{ind}^{\prime}_{=} : \prod_{A: \mathrm{Type}}\ \prod_{C: \prod_{x,y:A} x=y \to \mathrm{Type}}\ \left( \prod_{x:A} C(x,x,\mathrm{refl_x}) \right) \to \left( \prod_{x,y: A}\ \prod_{p: x=y} C(x,y) \right)$$

then you can prove via path induction for $\mathrm{ind}_=$ that any $\varpi : \mathrm{ind}_= =\mathrm{ind}^{\prime}_=$ will induce a dependent equality between any elements defined by the same formula, with either $\mathrm{ind}_=$ or $\mathrm{ind}^{\prime}_=$ chosen as interpretation of path induction.

I should note that there is basically the same problem with any type or element that we define in HoTT. For example, when we speak about $1$ we usually mean simply a point (final object of modelling category in general), but in fact this cannot be proven inside HoTT. What we can prove is that $1$ must be a contractible space with a distinguished point $e:1$. In the current implementation of HoTT there is simply no way to say that any other global element of $1$ is $e$ (and probably there shouldn't even be a way to state this). Similarly, $A+B$ is any space homotopy equivalent to the coproduct, although the symbol itself stands for a specific choice of such space. $\Bbb N$ is only guaranteed to have a countable number of contractible components, but similarly to $1$ there is no way to either state or prove that all of them are just points.

This means that induction for these spaces is also a priory non-unique. For example, for a contractible space obviously we can extend any section over the base point $e:1$ to the section over the whole space, but there are very many such choices. We pick one of them when we construct a model and call it $\mathrm{ind}_1$ (universally, i.e. for all type families at once). While we can prove that any other such choice is equal to $\mathrm{ind}_1$ (i.e. for any $\mathrm{ind}^\prime_1$ with tautological action over base point we can prove $\varphi: \mathrm{ind}_1 = \mathrm{ind}^\prime_1$, so the space of choices is in fact contactible), we cannot state or prove that the choice is unique in a classical sense.

Compare it with the folklore definition of homotopy limits/colimits, if you are familiar with $(\infty,1)$-categories. A homotopy limit $\lim F$ of a diagram $F$ is a (homotopy coherent) cone over $F$, such that for any other cone $D$ over $F$ there is a contractible space of maps $D\to \lim F$ making the obvious diagram (homotopy) commutative: $$\begin{matrix} D & \to & \lim F \\ & \searrow & \downarrow \\ & & B \end{matrix}$$

Your question is also discussed here. You can also post questions on the HoTT amateurs mailing list.

N.B.: One could ask if this non-uniqueness of choices could be further reduced on the level of formalism. Which of the defined objects can be stated definitionally equal? E.g. can we state that $a: 1 \vdash a \equiv e : 1$ ? Or that $1$ is defined uniquely? In some cases the answer seems to be yes, in many - no. Logically, such choices can break decidability of type-checking. Geometrically, we could impose impossibly harsh conditions on our spaces, building up from wrong intuition and missing the ways our symbols can be interpreted. In general it is an open problem.

I'm an amateur HoTT guy, so I'll try to complement Moses' already great answer. Let me take the type $A\times B$ as an example. The basic principle of constructive type theory, as outlined by Martin-Löf, is that *every element of $A\times B$ is described as being in the image of the constructor: $$\mathrm{pair}\ :\ A\rightarrow B\rightarrow A\times B$$ This philosophy allows us to define elimination: to build a function $f$ out of $A\times B$, it suffices to describe its action on the image of $\mathrm{pair}$.

But since $\mathrm{pair}$ is a constructor (and so is in particular injective), this means exactly that to build a function $f:A\times B\rightarrow C$, it suffices to describe it's action on a pair of elements in $A$ and $B$, so $$f':A\rightarrow B\rightarrow C$$ is sufficient to describe such an $f$. In conclusion, there is a canonical way to define functions out of $A\times B$, and this can be encapsulated in the type $$(A\rightarrow B\rightarrow C)\rightarrow(A\times B\rightarrow C)$$ but this is exactly the type of $\mathrm{ind}_{A\times B}$.

But this is only half of the story: what happens if this newly constructed $f$ is applied to a given $\mathrm{pair}(a,b)$? Well then $f$ should agree with its defining function $f'$, i.e. $$f(\mathrm{pair}(a,b))\ :=\ f'\ a\ b$$ i.e. $$\mathrm{ind}_{A\times B}\ f'\ \mathrm{pair}(a,b)\ :=\ f'\ a\ b$$ and this should hold definitionally (or computationally), which means the two should be completely interchangeable in all situations (which is much different from the $=$ in HoTT).

So you see that the definition of an eliminator for inductive type with given constructors comes in 2 steps:

1. an existence principle, which describes the type of $\mathrm{ind}$.

2. a coherence principle which defines the computational behavior of $\mathrm{ind}$. In category theory, this would correspond to uniqueness of the eliminator in some sense.

Let me argue that this is the same for the $=_A$ type. We want to build, given $x,y:A$ and $p:x=y$, an element of $C$ (we're forgetting the dependencies for simplification). To do that, we need to assume that $p$ was built using a constructor for the type $x=y$, which can only be $\mathrm{refl}(z)$ for some $z$. This means that to give a function $$f:\Pi x, y:A, x=y\rightarrow C$$ it suffices to give a function $$f':\Pi z:A, C$$ which is defined for $\mathrm{refl}(z)$ (again, forgetting the dependencies in $C$).

Now what does the coherence principle say? Well simply that if applied to a known constructor, $f$ should behave like $f'$, which means $$f\ z\ z\ \mathrm{refl}(z):= f'\ z$$

But that's exactly what you have above! The same principle that gave us the existence and coherence for the eliminator of $A\times B$ gives us the existence and coherence for the eliminator of $=_A$.