17
$\begingroup$

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"?

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

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.

$\endgroup$
  • $\begingroup$ I believe this answer is now (partially) out of date $\endgroup$ – WorldSEnder Oct 2 at 0:58
  • $\begingroup$ Indeed, in the mean time cubical type theory gave a postive answer: there is a constructive model of Univalent type theory. $\endgroup$ – Andrej Bauer Oct 2 at 10:54
7
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jul 30 '14 at 14:34
  • 2
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jul 30 '14 at 14:52
3
$\begingroup$

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$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.