If we endow intensional type theory with a homotopical interpretation (on a philosophical/ontological level), then the elimination rule for intensional identity types (also known as ), expresses the principle of path induction.
Recall the rule, viz.
We can think of the type as a mathematical or topological space, and of the terms as points of that space. Then, any can be thought of as a path in the space , with endpoints and .
The eliminator says that we can do induction on paths. That is: if we want to prove a motive which depends on two points and a path between these two points, then we may assume that the points are definitonally equal, and that the path between them is definitionally reflexivity. If we can prove that way, then we can prove given any path in .
In a sense, the path induction rule is just a "plain old" induction principle for an indexed inductive type: the only constructor for paths is . Thus, in order to inhabit the type family , it suffices to only inhabit it for the case . (NB: it is very important that and are free variables here. We can accept the case where one of them isn't, but not both. If both and are some specified term, then the above description leads to a proof of UIP.)
However, the surprising thing about Homotopy Type Theory is that the path induction rule remains sound despite the addition of further constructors for identity types -other than reflexivity! Recall that these come from the univalence axiom and higher inductive types.
Based path induction refers to the following alternative to the eliminator:
In words: if we are given a point , to prove a motive that depends on an arbitrary point that is equal to , as witnessed by , then it suffices to assume that and are definitionally equal, and is reflexivity.
Compared to path induction, is based because one of the endpoints of the path is fixed to be a specific term .
We quote the following passage from the bibliography of Chapter 1 of the HoTT book:
The path induction principle for identity types was formulated by Martin-Löf [ML98]. The
based path induction rule in the setting of Martin-Löf type theory is due to Paulin-Mohring
[PM93]; it can be seen as an intensional generalization of the concept of “pointwise functionality”
for hypothetical judgments from NuPRL [CAB+86, Section 8.1]. The fact that Martin-Löf’s rule
implies Paulin-Mohring’s was proved by Streicher using Axiom K (see §7.2), by Altenkirch and
Goguen as in §1.12, and finally by Hofmann without universes (as in Exercise 1.7); see [Str93,
§1.3 and Addendum].
Paulin-Mohring, Christine. 1993. ‘Inductive Definitions in the System Coq Rules and Properties’. In Typed Lambda Calculi and Applications, edited by Marc Bezem and Jan Friso Groote, 664:328–45. Lecture Notes in Computer Science. Berlin/Heidelberg: Springer-Verlag. https://doi.org/10.1007/BFb0037116.
@incollection{paulin-mohring_1993,
address = {Berlin/Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Inductive definitions in the system {Coq} rules and properties},
volume = {664},
isbn = {978-3-540-56517-8},
urldate = {2020-11-26},
booktitle = {Typed {Lambda} {Calculi} and {Applications}},
publisher = {Springer-Verlag},
author = {Paulin-Mohring, Christine},
editor = {Bezem, Marc and Groote, Jan Friso},
year = {1993},
doi = {10.1007/BFb0037116},
pages = {328--345}
}