1.12 Identity types
While the previous constructions can be seen as generalizations of standard set theoretic constructions, our way of handling identity seems to be specific to type theory. According to the propositions-as-types conception, the proposition that two elements of the same type are equal must correspond to some type. Since this proposition depends on what and are, these equality types or identity types must be type families dependent on two copies of .
We may write the family as , so that is the type representing the proposition of equality between and . Once we are familiar with propositions-as-types, however, it is convenient to also use the standard equality symbol for this; thus “” will also be a notation for the type corresponding to the proposition that equals . For clarity, we may also write “” to specify the type . If we have an element of , we may say that and are equal, or sometimes propositionally equal if we want to emphasize that this is different from the judgmental equality discussed in §1.1 (http://planetmath.org/11typetheoryversussettheory).
Just as we remarked in §1.11 (http://planetmath.org/111propositionsastypes) that the propositions-as-types versions of “or” and “there exists” can include more information than just the fact that the proposition is true, nothing prevents the type from also including more information. Indeed, this is the cornerstone of the homotopical interpretation, where we regard witnesses of as paths or equivalences between and in the space . Just as there can be more than one path between two points of a space, there can be more than one witness that two objects are equal. Put differently, we may regard as the type of identifications of and , and there may be many different ways in which and can be identified. We will return to the interpretation in http://planetmath.org/node/87569Chapter 2; for now we focus on the basic rules for the identity type. Just like all the other types considered in this chapter, it will have rules for formation, introduction, elimination, and computation, which behave formally in exactly the same way.
The formation rule says that given a type and two elements , we can form the type in the same universe. The basic way to construct an element of is to know that and are the same. Thus, the introduction rule is a dependent function
In particular, this means that if and are judgmentally equal, , then we also have an element . This is well-typed because means that also the type is judgmentally equal to , which is the type of .
The induction principle (i.e. the elimination rule) for the identity types is one of the most subtle parts of type theory, and crucial to the homotopy interpretation. We begin by considering an important consequence of it, the principle that “equals may be substituted for equals,” as expressed by the following:
- Indiscernability of identicals:
For every family
there is a function
This says that every family of types respects equality, in the sense that applying to equal elements of also results in a function between the resulting types. The displayed equality states that the function associated to reflexivity is the identity function (and we shall see that, in general, the function is always an equivalence of types).
Indiscernability of identicals can be regarded as a recursion principle for the identity type, analogous to those given for booleans and natural numbers above. Just as gives a specified map for any other type of a certain sort, indiscernability of identicals gives a specified map from to certain other reflexive, binary relations on , namely those of the form for some unary predicate . We could also formulate a more general recursion principle with respect to reflexive relations of the more general form . However, in order to fully characterize the identity type, we must generalize this recursion principle to an induction principle, which not only considers maps out of but also families over it. Put differently, we consider not only allowing equals to be substituted for equals, but also taking into account the evidence for the equality.
|Title||1.12 Identity types|