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 $a, b : A$ are equal must correspond to some type. Since this proposition depends on what $a$ and $b$ are, these equality types or identity types must be type families dependent on two copies of $A$ .

We may write the family as $\mathsf{Id}_{A}:A\to A\to\mathcal{U}$ , so that $\mathsf{Id}_{A}(a,b)$ is the type representing the proposition of equality between $a$ and $b$ . Once we are familiar with propositions-as-types, however, it is convenient to also use the standard equality symbol for this; thus “ $a=b$ ” will also be a notation for the type $\mathsf{Id}_{A}(a,b)$ corresponding to the proposition that $a$ equals $b$ . For clarity, we may also write “ $a=_{A}b$ ” to specify the type $A$ . If we have an element of $a=_{A}b$ , we may say that $a$ and $b$ are equal, or sometimes propositionally equal if we want to emphasize that this is different from the judgmental equality $a\equiv b$ 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 $a=b$ from also including more information. Indeed, this is the cornerstone of the homotopical interpretation, where we regard witnesses of $a=b$ as paths or equivalences between $a$ and $b$ in the space $A$ . 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 $a=b$ as the type of identifications of $a$ and $b$ , and there may be many different ways in which $a$ and $b$ 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 $A:\mathcal{U}$ and two elements $a, b : A$ , we can form the type $(a=_{A}b):\mathcal{U}$ in the same universe. The basic way to construct an element of $a=b$ is to know that $a$ and $b$ are the same. Thus, the introduction rule is a dependent function

$\mathsf{refl}:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{% (a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(a=_{A}a)$

called reflexivity, which says that every element of $A$ is equal to itself (in a specified way). We regard $\mathsf{refl}_{a}$ as being the constant path at the point $a$ .

In particular, this means that if $a$ and $b$ are judgmentally equal, $a\equiv b$ , then we also have an element $\mathsf{refl}_{a}:a=_{A}b$ . This is well-typed because $a\equiv b$ means that also the type $a=_{A}b$ is judgmentally equal to $a=_{A}a$ , which is the type of $\mathsf{refl}_{a}$ .

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

$C:A\to\mathcal{U}$

there is a function

$f:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=_{A}y)}\,}{\mathchoice{{\textstyle% \prod_{(p:x=_{A}y)}}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{% A}y)}}}{\mathchoice{{\textstyle\prod_{(p:x=_{A}y)}}}{\prod_{(p:x=_{A}y)}}{% \prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}}{\mathchoice{{\textstyle\prod_{(p:x=% _{A}y)}}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}{\prod_{(p:x=_{A}y)}}}C(x)% \to C(y)$

such that

$f(x,x,\mathsf{refl}_{x}):\!\!\equiv\mathsf{id}_{C(x)}.$

This says that every family of types $C$ respects equality, in the sense that applying $C$ to equal elements of $A$ 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 $f(x,y,p):C(x)\to C(y)$ 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 $\mathsf{rec}_{\mathbb{N}}$ gives a specified map $\mathbb{N}\to C$ for any other type $C$ of a certain sort, indiscernability of identicals gives a specified map from $x=_{A}y$ to certain other reflexive, binary relations on $A$ , namely those of the form $C(x)\to C(y)$ for some unary predicate $C(x)$ . We could also formulate a more general recursion principle with respect to reflexive relations of the more general form $C(x,y)$ . 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 $x=_{A}y$ 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 $p$ for the equality.

Title	1.12 Identity types
\metatable