1.12 Identity types

While the previous constructions can be seen as generalizationsPlanetmathPlanetmath of standard set theoretic constructions, our way of handling identity seems to be specific to type theoryPlanetmathPlanetmath. According to the propositions-as-types conception, the propositionPlanetmathPlanetmathPlanetmath 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 𝖨𝖽A:Aβ†’A→𝒰, so that 𝖨𝖽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 𝖨𝖽A⁒(a,b) corresponding to the proposition that a equals b. For clarity, we may also write β€œa=Ab” to specify the type A. If we have an element of a=Ab, 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≑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 interpretationMathworldPlanetmathPlanetmath, 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:𝒰 and two elements a,b:A, we can form the type (a=Ab):𝒰 in the same universePlanetmathPlanetmath. 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


called reflexivityMathworldPlanetmath, which says that every element of A is equal to itself (in a specified way). We regard 𝗋𝖾𝖿𝗅a as being the constant path at the point a.

In particular, this means that if a and b are judgmentally equal, a≑b, then we also have an element 𝗋𝖾𝖿𝗅a:a=Ab. This is well-typed because a≑b means that also the type a=Ab is judgmentally equal to a=Aa, which is the type of 𝗋𝖾𝖿𝗅a.

The inductionMathworldPlanetmath 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


such that


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)β†’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 numbersMathworldPlanetmath above. Just as 𝗋𝖾𝖼ℕ gives a specified map β„•β†’C for any other type C of a certain sort, indiscernability of identicals gives a specified map from x=Ay to certain other reflexiveMathworldPlanetmath, binary relationsMathworldPlanetmath on A, namely those of the form C⁒(x)β†’C⁒(y) for some unary predicateMathworldPlanetmath 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=Ay 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