[Solved]: Is path induction constructive?

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.