2.11 Identity type

Just as the type a=Aa is characterized up to isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, with a separate “definition” for each A, there is no simple characterization of the type p=a=Aaq of paths between paths p,q:a=Aa. However, our other general classes of theorems do extend to identity types, such as the fact that they respect equivalence.

Theorem 2.11.1.

If f:AB is an equivalence, then for all a,a:A, so is


Let f-1 be a quasi-inverse of f, with homotopiesMathworldPlanetmathPlanetmath

α:b:B(f(f-1(b))=b)  and  β:a:A(f-1(f(a))=a).

The quasi-inverse of 𝖺𝗉f is, essentially,


However, in order to obtain an element of a=Aa from 𝖺𝗉f-1(q), we must concatenate with the paths βa-1 and βa on either side. To show that this gives a quasi-inverse of 𝖺𝗉f, on one hand we must show that for any p:a=Aa 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 q:f(a)=Bf(a) 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 inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath paths):

𝖺𝗉f(βa-1\centerdot𝖺𝗉f-1(q)\centerdotβa) =αf(a)-1\centerdotαf(a)\centerdot𝖺𝗉f(βa-1\centerdot𝖺𝗉f-1(q)\centerdotβa)\centerdotαf(a)-1\centerdotαf(a)

Thus, if for some type A we have a full characterization of a=Aa, the type p=a=Aaq is determined as well. For example:

  • Paths p=q, where p,q:w=A×Bw, are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to pairs of paths

  • Paths p=q, where p,q:f=(x:A)B(x)g, are equivalent to homotopies


Next we consider transport in families of paths, i.e. transport in C:A𝒰 where each C(x) is an identity type. The simplest case is when C(x) is a type of paths in A itself, perhaps with one endpoint fixed.

Lemma 2.11.2.

For any A and a:A, with p:x1=x2, we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍x(a=x)(p,q) =q\centerdotp for q:a=x1,
𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍x(x=a)(p,q) =p-1\centerdotq for q:x1=a,
𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍x(x=x)(p,q) =p-1\centerdotq\centerdotp for q:x1=x1.

Path inductionMathworldPlanetmath on p, followed by the unit laws for composition. ∎

In other words, transporting with xc=x is post-composition, and transporting with xx=c is contravariant pre-composition. These may be familiar as the functorial actions of the covariant and contravariant hom-functors hom(c,) and hom(,c) in category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

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:

Theorem 2.11.3.

For f,g:AB, with p:a=Aa and q:f(a)=Bg(a), we have


Because 𝖺𝗉(xx) is the identity function and 𝖺𝗉(xc) (where c is a constant) is 𝗋𝖾𝖿𝗅c, Lemma 1 (http://planetmath.org/211identitytype#Thmlem1) is a special case. A yet more general version is when B can be a family of types indexed on A:

Theorem 2.11.4.

Let B:AU and f,g:(x:A)B(x), with p:a=Aa and q:f(a)=B(a)g(a). 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.

Theorem 2.11.5.

For p:a=Aa with q:a=a and r:a=a, we have


Path induction on p, followed by the fact that composing with the unit equalities q\centerdot1=q and r=1\centerdotr 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