5.8 Identity types and identity systems
We now wish to point out that the identity types, which play so central a role in homotopy type theory, may also be considered to be defined inductively. Specifically, they are an “inductive family” with indices, in the sense of §5.7 (http://planetmath.org/57generalizationsofinductivetypes). In fact, there are two ways to describe identity types as an inductive family, resulting in the two induction principles described in http://planetmath.org/node/87533Chapter 1, path induction and based path induction.
for any , an element .
By analogy with the other inductive families, we may extract the induction principle from this definition. It states that given any along with , there exists such that . This is exactly the path induction principle for identity types.
For the second definition, we consider one element to be a parameter along with , and we inductively define a family , with one index belonging to , by the following constructor:
an element .
Note that because was fixed as a parameter, the constructor does not appear inside the inductive definition as a function, but only an element. The induction principle for this definition says that given along with an element , there exists with . This is exactly the based path induction principle for identity types.
The view of identity types as inductive types has historically caused some confusion, because of the intuition mentioned in §5.1 (http://planetmath.org/51introductiontoinductivetypes) that all the elements of an inductive type should be obtained by repeatedly applying its constructors. For ordinary inductive types such as and , this is the case: we saw in (http://planetmath.org/18thetypeofbooleans#1 ) that indeed every element of is either or , and similarly one can prove that every element of is either or a successor.
However, this is not true for identity types: there is only one constructor , but not every path is equal to the constant path. More precisely, we cannot prove, using only the induction principle for identity types (either one), that every inhabitant of is equal to . In order to actually exhibit a counterexample, we need some additional principle such as the univalence axiom — recall that in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6) we used univalence to exhibit a particular path which is not equal to .
The point is that, as validated by the study of homotopy-initial algebras, an inductive definition should be regarded as freely generated by its constructors. Of course, a freely generated structure may contain elements other than its generators: for instance, the free group on two symbols and contains not only and but also words such as , , and . In general, the elements of a free structure are obtained by applying not only the generators, but also the operations of the ambient structure, such as the group operations if we are talking about free groups.
In the case of inductive types, we are talking about freely generated types — so what are the “operations” of the structure of a type? If types are viewed as like sets, as was traditionally the case in type theory, then there are no such operations, and hence we expect there to be no elements in an inductive type other than those resulting from its constructors. In homotopy type theory, we view types as like spaces or -groupoids, in which case there are many operations on the paths (concatenation, inversion, etc.) — this will be important in http://planetmath.org/node/87579Chapter 6 — but there are still no operations on the objects (elements). Thus, it is still true for us that, e.g., every element of is either or , and every element of is either or a successor.
However, as we saw in http://planetmath.org/node/87569Chapter 2, viewing types as -groupoids entails also viewing functions as functors, and this includes type families . Thus, the identity type , viewed as an inductive type family, is actually a freely generated functor . Specifically, it is the functor freely generated by one element . And a functor does have operations on objects, namely the action of the morphisms (paths) of .
In category theory, the Yoneda lemma tells us that for any category and object , the functor freely generated by an element of is the representable functor . Thus, we should expect the identity type to be this representable functor, and this is indeed exactly how we view it: is the space of morphisms (paths) in from to .
One reason for viewing identity types as inductive families is to apply the uniqueness principles of §5.2 (http://planetmath.org/52uniquenessofinductivetypes),§5.5 (http://planetmath.org/55homotopyinductivetypes). Specifically, we can characterize the family of identity types of a type , up to equivalence, by giving another family of types over satisfying the same induction principle. This suggests the following definitions and theorem.
Note that the equivalences 123 are a version of Lemma 5.5.4 (http://planetmath.org/55homotopyinductivetypes#Thmprelem1) for identity types , regarded as inductive families varying over one element of . Of course, 2–4 are mere propositions, so that logical equivalence implies actual equivalence. (Condition 1 is also a mere proposition, but we will not prove this.)
First, assume 1 and let be a pointed predicate. Define and . Since is an identity system, we have with ; hence is inhabited. Now suppose , and define , and let . Then again since is an identity system, we have such that . By the characterization of paths in -types and path types, these data yield an equality . Hence is an inhabited mere proposition, and thus contractible; so 2 holds.
Now suppose 2, and define with . Then is a pointed predicate, and is a pointed family of maps from to . By assumption, is contractible, hence inhabited, so there also exists a pointed family of maps from to . And the composites in either direction are pointed families of maps from to and from to , respectively, hence equal to identities since and are contractible. Thus 3 holds.
Now supposing 3, condition 4 follows from Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), using the fact that -types respect equivalences (the “if” direction of Theorem 4.7.7 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm4)).
We can deduce a similar result for identity types , regarded as a family varying over two elements of .
An identity system over a type is a family equipped with a function such that for any type family and , there exists a function such that for all .
For equipped with , the following are logically equivalent.
is an identity system over .
For all , the pointed predicate is an identity system at .
For any and , the type
For any , the map is an equivalence.
For any , the type is contractible.
The equivalence 12 follows exactly the proof of equivalence between the path induction and based path induction principles for identity types; see §1.12 (http://planetmath.org/112identitytypes). The equivalence with 4 and 5 then follows from Theorem 5.8.2 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm1), while 3 is straightforward. ∎
One reason this characterization is interesting is that it provides an alternative way to state univalence and function extensionality. The univalence axiom for a universe says exactly that the type family
together with satisfies Theorem 5.8.4 (http://planetmath.org/58identitytypesandidentitysystems#Thmprethm2)4. Therefore, it is equivalent to the corresponding version of 1, which we can state as follows.
Corollary 5.8.5 (Equivalence induction).
Given any type family and function , there exists such that for all .
In other words, to prove something about all equivalences, it suffices to prove it about identity maps. We have already used this principle (without stating it in generality) in Lemma 4.1.1 (http://planetmath.org/41quasiinverses#Thmprelem1).
Similarly, function extensionality says that for any , the type family
Corollary 5.8.6 (Homotopy induction).
Given any and , there exists
such that for all .
|Title||5.8 Identity types and identity systems|