The independence of path induction

Question

In §1.12 of the Homotopy type theory book, it is mentioned that indiscernibility of identicals is a consequence of path induction. More precisely, for each type $C$ dependent over a type $A$, there is a term $$\mathsf{transport} : \prod_{a_0, a_1 : A} \prod_{p : a_0 =_A a_1} C (a_0) \to C (a_1)$$ such that $\mathsf{transport} (a, a, \mathsf{refl}) \equiv \mathsf{id}_{C (a)}$, which is manifestly an instance of the general path induction principle, which constructs for each type $B$ dependent over $\sum_{a_0, a_1 : A} a_0 =_A a_1$ and each $s : \prod_{a : A} B (a, a, \mathsf{refl})$ a term $$\mathsf{ind}(s) : \prod_{a_0, a_1 : A} \prod_{p : a_0 =_A a_1} B (a_0, a_1, p)$$ such that $\mathsf{ind}(s, a, a, \mathsf{refl}) \equiv s (a)$.

Question. Is path induction strictly stronger than indiscernibility of identicals? (Or, does there exist a model of intensional type theory where the propositional equality satisfies indiscernibility of identicals but not path induction?)

I ask because the built-in eq type in Coq is defined as an inductive type whose induction principle is indiscernibility of identicals, rather than path induction. Coq is sufficiently rich to allow the path induction principle as well; however, it doesn't seem to be derived from the indiscernibility of identicals but rather by using pattern matching directly.

Answer 1

The problem with postulating only $\mathsf{transport}$ is that it is too weak to characterize the identity type up to equivalence. Let me define another type, called $\mathsf{doubleId}$, which has a $\mathsf{doubleRefl}$ and a $\mathsf{doubleTransport}$ satisfying the same rules as $\mathsf{refl}$ and $\mathsf{transport}$, but is not equivalent to the identity type.

We can take our type to be two copies of the identity type: $$\mathsf{doubleId}(a,b) \mathrel{{:}{\equiv}} (a = b) + (a = b).$$ There are two choices for $\mathsf{doubleRefl}$, so let us pick $\mathsf{inl}(\mathsf{refl})$. This type has a $\mathsf{transport}$-like eliminator, defined by $$\mathsf{doubleTransport}(a_0, a_1, \mathsf{inl}(p)) \mathrel{{:}{\equiv}} \mathsf{transport}(a_0, a_1, p)$$ $$\mathsf{doubleTransport}(a_0, a_1, \mathsf{inr}(p)) \mathrel{{:}{\equiv}} \mathsf{transport}(a_0, a_1, p),$$ but it does not have an $\mathsf{ind}$-like eliminator. For suppose we had a $\mathsf{doubleInd}$. Define $B$ over $\sum_{a_0, a_1 : A} \mathsf{doubleId}(a_0, a_1)$ by $$B(a_0, a_1, \mathsf{inl}(p)) \mathrel{{:}{\equiv}} \mathsf{unit}$$ $$B(a_0, a_1, \mathsf{inr}(p)) \mathrel{{:}{\equiv}} \mathsf{empty}$$ Now we have $s : \prod_{a : A} B(a, a, \mathsf{doubleRefl})$, namely the map $\lambda a . \star$ (where $\star$ is the only element of $\mathsf{unit}$). If we had $\mathsf{doubleInd}$ then we could produce an element of $B(a, a, \mathsf{inr}(\mathsf{refl}))$, and thereby inhabit $\mathsf{empty}$.

Your question can be asked more generally: does the non-dependent eliminator (in your case $\mathsf{transport}$) suffice, or do we need the dependent one (in your case $\mathsf{ind}$)? The answer is: you need the dependent one, otherwise the type is not fixed up to equivalence. It is a good exercise to try this with the circle.