1.12.1 Path Induction


The inductionMathworldPlanetmath principle for the identity type is called path induction, in view of the homotopical interpretationMathworldPlanetmathPlanetmath to be explained in the introduction to http://planetmath.org/node/87569Chapter 2. It can be seen as stating that the family of identity types is freely generated by the elements of the form 𝗋𝖾𝖿𝗅x:x=x.

Path induction:

Given a family

C:∏x,y:A(x=Ay)→𝒰

and a function

c:∏x:AC⁒(x,x,𝗋𝖾𝖿𝗅x),

there is a function

f:∏(x,y:A)∏(p:x=Ay)C⁒(x,y,p)

such that

f(x,x,𝗋𝖾𝖿𝗅x):≑c(x).

Note that just like the induction principles for productsPlanetmathPlanetmathPlanetmath, coproducts, natural numbersMathworldPlanetmath, and so on, path induction allows us to define specified functions which exhibit appropriate computational behavior. Just as we have the function f:β„•β†’C defined by recursion from c0:C and cs:β„•β†’Cβ†’C, which moreover satisfies f⁒(0)≑c0 and f⁒(π—Œπ—Žπ–Όπ–Όβ’(n))≑cs⁒(n,f⁒(n)), we have the function f:∏(x,y:A)∏(p:x=Ay)C⁒(x,y,p) defined by path induction from c:∏(x:A)C⁒(x,x,𝗋𝖾𝖿𝗅x), which moreover satisfies f⁒(x,x,𝗋𝖾𝖿𝗅x)≑c⁒(x).

To understand the meaning of this principle, consider first the simpler case when C does not depend on p. Then we have C:Aβ†’A→𝒰, which we may regard as a predicateMathworldPlanetmath depending on two elements of A. We are interested in knowing when the propositionPlanetmathPlanetmath C⁒(x,y) holds for some pair of elements x,y:A. In this case, the hypothesisMathworldPlanetmath of path induction says that we know C⁒(x,x) holds for all x:A, i.e.Β that if we evaluate C at the pair x,x, we get a true proposition β€” so C is a reflexive relation. The conclusionMathworldPlanetmath then tells us that C⁒(x,y) holds whenever x=y. This is exactly the more general recursion principle for reflexive relations mentioned above.

The general, inductive form of the rule allows C to also depend on the witness p:x=y to the identityPlanetmathPlanetmathPlanetmathPlanetmath between x and y. In the premise, we not only replace x,y by x,x, but also simultaneously replace p by reflexivity: to prove a property for all elements x,y and paths p:x=y between them, it suffices to consider all the cases where the elements are x,x and the path is 𝗋𝖾𝖿𝗅x:x=x. If we were viewing types just as sets, it would be unclear what this buys us, but since there may be many different identifications p:x=y between x and y, it makes sense to keep track of them in considering families over the type x=Ay. In http://planetmath.org/node/87569Chapter 2 we will see that this is very important to the homotopyMathworldPlanetmathPlanetmath interpretation.

If we package up path induction into a single function, it takes the form:

𝗂𝗇𝖽=A:∏(C:∏(x,y:A)(x=Ay)→𝒰)(∏(x:A)C⁒(x,x,𝗋𝖾𝖿𝗅x))β†’βˆ(x,y:A)∏(p:x=Ay)C⁒(x,y,p)

with the equality

𝗂𝗇𝖽=A(C,c,x,x,𝗋𝖾𝖿𝗅x):≑c(x).

The function 𝗂𝗇𝖽=A is traditionally called J. We leave it as an easy exercise to show that indiscernability of identicals follows from path induction.

Given a proof p:a=b, path induction requires us to replace both a and b with the same unknown element x; thus in order to define an element of a family C, for all pairs of elements of A, it suffices to define it on the diagonal. In some proofs, however, it is simpler to make use of an equation p:a=b by replacing all occurrences of b with a (or vice versa), because it is sometimes easier to do the remainder of the proof for the specific element a mentioned in the equality than for a general unknown x. This motivates a second induction principle for identity types, which says that the family of types a=Ax is generated by the element 𝗋𝖾𝖿𝗅a:a=a. As we show below, this second principle is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the first; it is just sometimes a more convenient formulation.

Based path induction:

Fix an element a:A, and suppose given a family

C:∏x:A(a=Ax)→𝒰

and an element

c:C⁒(a,𝗋𝖾𝖿𝗅a).

Then we obtain a function

f:∏(x:A)∏(p:a=x)C⁒(x,p)

such that

f(a,𝗋𝖾𝖿𝗅a):≑c.

Here, C⁒(x,p) is a family of types, where x is an element of A and p is an element of the identity type a=Ax, for fixed a in A. The based path induction principle says that to define an element of this family for all x and p, it suffices to consider just the case where x is a and p is 𝗋𝖾𝖿𝗅a:a=a.

Packaged as a function, based path induction becomes:

𝗂𝗇𝖽=Aβ€²:∏(a:A)∏(C:∏(x:A)(a=Ax)→𝒰)C⁒(a,𝗋𝖾𝖿𝗅a)β†’βˆ(x:A)∏(p:a=Ax)C⁒(x,p)

with the equality

𝗂𝗇𝖽=Aβ€²(a,C,c,a,𝗋𝖾𝖿𝗅a):≑c.

Below, we show that path induction and based path induction are equivalent. Because of this, we will sometimes be sloppy and also refer to based path induction simply as β€œpath induction,” relying on the reader to infer which principle is meant from the form of the proof.

Remark 1.

Intuitively, the induction principle for the natural numbers expresses the fact that the only natural numbers are 0 and succ⁒(n), so if we prove a property for these cases, then we have proved it for all natural numbers. Applying this same reading to path induction, we might loosely say that path induction expresses the fact that the only path is refl, so if we prove a property for reflexivity, then we have proved it for all paths. However, this reading is quite confusing in the context of the homotopy interpretation of paths, where there may be many different ways in which two elements a and b can be identified, and therefore many different elements of the identity type! How can there be many different paths, but at the same time we have an induction principle asserting that the only path is reflexivity?

The key observation is that it is not the identity type that is inductively defined, but the identity family. In particular, path induction says that the family of types (x=Ay), as x,y vary over all elements of A, is inductively defined by the elements of the form reflx. This means that to give an element of any other family C⁒(x,y,p) dependent on a genericPlanetmathPlanetmathPlanetmath element (x,y,p) of the identity family, it suffices to consider the cases of the form (x,x,reflx). In the homotopy interpretation, this says that the type of triples (x,y,p), where x and y are the endpoints of the path p (in other words, the Ξ£-type βˆ‘(x,y:A)(x=y)), is inductively generated by the constant loops at each point x. In homotopy theory, the space corresponding to βˆ‘(x,y:A)(x=y) is the free path space β€” the space of paths in A whose endpoints may vary β€” and it is in fact the case that any point of this space is homotopicMathworldPlanetmath to the constant loop at some point, since we can simply retractMathworldPlanetmath one of its endpoints along the given path.

Similarly, based path induction says that for a fixed a:A, the family of types (a=Ay), as y varies over all elements of A, is inductively defined by the element refla. Thus, to give an element of any other family C⁒(y,p) dependent on a generic element (y,p) of this family, it suffices to consider the case (a,refla). Homotopically, this expresses the fact that the space of paths starting at some chosen point (the based path space at that point, which type-theoretically is βˆ‘(y:A)(a=y)) is contractible to the constant loop on the chosen point. Note that according to propositions-as-types, the type βˆ‘(y:A)(a=y) can be regarded as β€œthe type of all elements of A which are equal to a”, a type-theoretic version of the β€œsingleton subset” {a}.

Neither of these two principles provides a way to give an element of a family C⁒(p) where p has two fixed endpoints a and b. In particular, for a family C(p:a=Aa) dependent on a loop, we cannot apply path induction and consider only the case for C⁒(refla), and consequently, we cannot prove that all loops are reflexivity. Thus, inductively defining the identity family does not prohibit non-reflexivity paths in specific instances of the identity type. In other words, a path p:x=x may be not equal to reflexivity as an element of (x=x), but the pair (x,p) will nevertheless be equal to the pair (x,reflx) as elements of βˆ‘(y:A)(x=y).

Title 1.12.1 Path Induction
\metatable