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

𝖺𝗉f:(a=Aa)(f(a)=Bf(a)).
Proof.

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,

𝖺𝗉f-1:(f(a)=f(a))(f-1(f(a))=f-1(f(a))).

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

βa-1\centerdot𝖺𝗉f-1(𝖺𝗉f(p))\centerdotβa=p.

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

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

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)
=αf(a)-1\centerdot𝖺𝗉f(𝖺𝗉f-1(𝖺𝗉f(βa-1\centerdot𝖺𝗉f-1(q)\centerdotβa)))\centerdotαf(a)
=αf(a)-1\centerdot𝖺𝗉f(βa\centerdotβa-1\centerdot𝖺𝗉f-1(q)\centerdotβa\centerdotβa-1)\centerdotαf(a)
=αf(a)-1\centerdot𝖺𝗉f(𝖺𝗉f-1(q))\centerdotαf(a)
=q.

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

    𝖺𝗉𝗉𝗋1p=𝗉𝗋1w=A𝗉𝗋1w𝖺𝗉𝗉𝗋1qand𝖺𝗉𝗉𝗋2p=𝗉𝗋2w=B𝗉𝗋2w𝖺𝗉𝗉𝗋2q.
  • Paths p=q, where p,q:f=(x:A)B(x)g, are equivalent to homotopies

    x:A(𝗁𝖺𝗉𝗉𝗅𝗒(p)(x)=f(x)=g(x)𝗁𝖺𝗉𝗉𝗅𝗒(q)(x)).

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.
Proof.

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

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍xf(x)=Bg(x)(p,q)=f(a)=g(a)(𝖺𝗉fp)-1\centerdotq\centerdot𝖺𝗉gp.

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

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍xf(x)=B(x)g(x)(p,q)=(𝖺𝗉𝖽f(p))-1\centerdot𝖺𝗉(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍Ap)(q)\centerdot𝖺𝗉𝖽g(p).

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

(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍x(x=x)(p,q)=r)(q\centerdotp=p\centerdotr).
Proof.

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
\metatable