2.11 Identity type
Just as the type is characterized up to isomorphism, with a separate “definition” for each , there is no simple characterization of the type of paths between paths . However, our other general classes of theorems do extend to identity types, such as the fact that they respect equivalence.
If is an equivalence, then for all , so is
The quasi-inverse of is, essentially,
However, in order to obtain an element of from , we must concatenate with the paths and on either side. To show that this gives a quasi-inverse of , on one hand we must show that for any we have
This follows from the functoriality of and the naturality of homotopies, Lemma 2.2.4 (http://planetmath.org/22functionsarefunctors#Thmprelem4),Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2). On the other hand, we must show that for any we have
The proof of this is a little more involved, but each step is again an application of Lemma 2.2.4 (http://planetmath.org/22functionsarefunctors#Thmprelem4),Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2) (or simply canceling inverse paths):
Thus, if for some type we have a full characterization of , the type is determined as well. For example:
Paths , where , are equivalent to pairs of paths
Paths , where , are equivalent to homotopies
Next we consider transport in families of paths, i.e. transport in where each is an identity type. The simplest case is when is a type of paths in itself, perhaps with one endpoint fixed.
For any and , with , we have
In other words, transporting with is post-composition, and transporting with is contravariant pre-composition. These may be familiar as the functorial actions of the covariant and contravariant hom-functors and in category theory.
Combining Lemma 2.11.2 (http://planetmath.org/211identitytype#Thmprelem1),Lemma 2.3.8 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem7), we obtain a more general form:
For , with and , we have
Because is the identity function and (where is a constant) is , Lemma 1 (http://planetmath.org/211identitytype#Thmlem1) is a special case. A yet more general version is when can be a family of types indexed on :
Let and , with and . Then we have
Finally, as in §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom), for families of identity types there is another equivalent characterization of dependent paths.
For with and , we have
Path induction on , followed by the fact that composing with the unit equalities and is an equivalence. ∎
There are more general equivalences involving the application of functions, akin to Theorem 2.11.3 (http://planetmath.org/211identitytype#S0.Thmprethm2),Theorem 2.11.4 (http://planetmath.org/211identitytype#S0.Thmprethm3).
|Title||2.11 Identity type|