1.12.1 Path Induction
The induction principle for the identity type is called path induction, in view of the homotopical interpretation 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 .
- Path induction:
Given a family
and a function
there is a function
Note that just like the induction principles for products, coproducts, natural numbers, and so on, path induction allows us to define specified functions which exhibit appropriate computational behavior. Just as we have the function defined by recursion from and , which moreover satisfies and , we have the function defined by path induction from , which moreover satisfies .
To understand the meaning of this principle, consider first the simpler case when does not depend on . Then we have , which we may regard as a predicate depending on two elements of . We are interested in knowing when the proposition holds for some pair of elements . In this case, the hypothesis of path induction says that we know holds for all , i.e. that if we evaluate at the pair , we get a true proposition — so is a reflexive relation. The conclusion then tells us that holds whenever . This is exactly the more general recursion principle for reflexive relations mentioned above.
The general, inductive form of the rule allows to also depend on the witness to the identity between and . In the premise, we not only replace by , but also simultaneously replace by reflexivity: to prove a property for all elements and paths between them, it suffices to consider all the cases where the elements are and the path is . If we were viewing types just as sets, it would be unclear what this buys us, but since there may be many different identifications between and , it makes sense to keep track of them in considering families over the type . In http://planetmath.org/node/87569Chapter 2 we will see that this is very important to the homotopy interpretation.
If we package up path induction into a single function, it takes the form:
with the equality
The function is traditionally called . We leave it as an easy exercise to show that indiscernability of identicals follows from path induction.
Given a proof , path induction requires us to replace both and with the same unknown element ; thus in order to define an element of a family , for all pairs of elements of , it suffices to define it on the diagonal. In some proofs, however, it is simpler to make use of an equation by replacing all occurrences of with (or vice versa), because it is sometimes easier to do the remainder of the proof for the specific element mentioned in the equality than for a general unknown . This motivates a second induction principle for identity types, which says that the family of types is generated by the element . As we show below, this second principle is equivalent to the first; it is just sometimes a more convenient formulation.
- Based path induction:
Fix an element , and suppose given a family
and an element
Then we obtain a function
Here, is a family of types, where is an element of and is an element of the identity type , for fixed in . The based path induction principle says that to define an element of this family for all and , it suffices to consider just the case where is and is .
Packaged as a function, based path induction becomes:
with the equality
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.
Intuitively, the induction principle for the natural numbers expresses the fact that the only natural numbers are and , 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 , 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 and 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 , as vary over all elements of , is inductively defined by the elements of the form . This means that to give an element of any other family dependent on a generic element of the identity family, it suffices to consider the cases of the form . In the homotopy interpretation, this says that the type of triples , where and are the endpoints of the path (in other words, the -type ), is inductively generated by the constant loops at each point . In homotopy theory, the space corresponding to is the free path space — the space of paths in whose endpoints may vary — and it is in fact the case that any point of this space is homotopic to the constant loop at some point, since we can simply retract one of its endpoints along the given path.
Similarly, based path induction says that for a fixed , the family of types , as varies over all elements of , is inductively defined by the element . Thus, to give an element of any other family dependent on a generic element of this family, it suffices to consider the case . 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 ) is contractible to the constant loop on the chosen point. Note that according to propositions-as-types, the type can be regarded as “the type of all elements of which are equal to ”, a type-theoretic version of the “singleton subset” .
Neither of these two principles provides a way to give an element of a family where has two fixed endpoints and . In particular, for a family dependent on a loop, we cannot apply path induction and consider only the case for , 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 may be not equal to reflexivity as an element of , but the pair will nevertheless be equal to the pair as elements of .
|Title||1.12.1 Path Induction|