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.

  • 2
    $\begingroup$ FWIW, the reason that Coq's 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

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.

| cite | improve this answer | |

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.