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.

`eq`

only gets IOI as its "induction principle" is that`eq`

is valued in`Prop`

and Coq likes to pretend that`Prop`

consists of hProps (even though it doesn't). As you observed,`eq`

actually has the full correct induction principle of an identity type (implemented via pattern matching); it's just that because of`Prop`

, Coq hamstrings itself in the type of the function`eq_rect`

that it derives automatically from this principle. $\endgroup$ – Mike Shulman Sep 4 '13 at 22:29