PLS Lab

Path induction

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 \textsf{J}), expresses the principle of path induction.

Recall the \textsf{J} rule, viz.

\frac{
	\Gamma \vdash P : \textsf{Id}_A(M, N)
  \quad
  \Gamma, x : A, y : A, p : \textsf{Id}_A(x, y) \vdash C \textsf{ type}
  \quad
  \Gamma, z : A \vdash X : C[z, z, \textsf{refl}_A(z)/x, y, p]
}{
	\Gamma \vdash \textsf{J}_{x, y, p. C}(M, N, P, X) : C[M, N, P/x, y, p]
}

We can think of the type A as a mathematical or topological space, and of the terms M, N : A as points of that space. Then, any P : \textsf{Id}_A(M, N) can be thought of as a path in the space A, with endpoints M and N.

The \textsf{J} eliminator says that we can do induction on paths. That is: if we want to prove a motive C which depends on two points x, y : A and a path P : \textsf{Id}_A(M, N) 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 C that way, then we can prove C given any path in \textsf{Id}_A(M, N).

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 \textsf{refl}_M : \textsf{Id}_A(M, M). Thus, in order to inhabit the type family C(x, y, p), it suffices to only inhabit it for the case C(x, x, \textsf{refl}_A(x)). (NB: it is very important that x and y are free variables here. We can accept the case where one of them isn't, but not both. If both x and y 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

Based path induction refers to the following alternative to the \textsf{J} eliminator:

\frac{
	\Gamma \vdash P : \textsf{Id}_A(M, N)
  \quad
  \Gamma, y : A, p : \textsf{Id}_A(M, y) \vdash C \textsf{ type}
  \quad
  \Gamma, z : A \vdash X : C[z, \textsf{refl}_A(z)/y, p]
}{
	\Gamma \vdash \textsf{B}^M_{y, p. C}(N, P, X) : C[N, P/y, p]
}

In words: if we are given a point M : A, to prove a motive C that depends on an arbitrary point y : A that is equal to M, as witnessed by P : \textsf{Id}_A(M, y), then it suffices to assume that x and y are definitionally equal, and P is reflexivity.

Compared to path induction, \textsf{B} is based because one of the endpoints of the path P is fixed to be a specific term M.

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.

References

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}
}