2.11 Identity type

Just as the type $a{=}_A{a}^{\prime }$ is characterized up to isomorphism, with a separate “definition” for each $A$, there is no simple characterization of the type $p{=}_{a{=}_A{a}^{\prime }}q$ of paths between paths $p,q:a{=}_A{a}^{\prime }$. 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\mathrm{:}A\mathrm{\to }B$ is an equivalence, then for all $a\mathrm{,}{a}^{\mathrm{\prime }}\mathrm{:}A$, so is

$${\mathrm{𝖺𝗉}}_f:(a{=}_A{a}^{\prime })\to (f(a){=}_{B}f(a^{\prime })).$$

Proof.

Let $f^{-1}$ be a quasi-inverse of $f$, with homotopies

$$\alpha :\prod _{b:B}(f(f^{-1}(b))=b)\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}\beta :\prod _{a:A}(f^{-1}(f(a))=a).$$

The quasi-inverse of ${\mathrm{𝖺𝗉}}_f$ is, essentially,

$${\mathrm{𝖺𝗉}}_{f^{-1}}:(f(a)=f(a^{\prime }))\to (f^{-1}(f(a))=f^{-1}(f(a^{\prime }))).$$

However, in order to obtain an element of $a{=}_A{a}^{\prime }$ from ${\mathrm{𝖺𝗉}}_{f^{-1}}(q)$, we must concatenate with the paths $\beta _a{}^{-1}$ and ${\beta }_{a^{\prime }}$ on either side. To show that this gives a quasi-inverse of ${\mathrm{𝖺𝗉}}_f$, on one hand we must show that for any $p:a{=}_A{a}^{\prime }$ we have

$$\beta _a{}^{-1}{\mathrm{𝖺𝗉}}_{f^{-1}}({\mathrm{𝖺𝗉}}_f(p)){\beta }_{a^{\prime }}=p.$$

This follows from the functoriality of $\mathrm{𝖺𝗉}$ 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){=}_{B}f(a^{\prime })$ we have

$${\mathrm{𝖺𝗉}}_f\left(\beta _a{}^{-1}{\mathrm{𝖺𝗉}}_{f^{-1}}(q){\beta }_{a^{\prime }}\right)=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 inverse paths):

${\mathrm{𝖺𝗉}}_f\left(\beta _a{}^{-1}{\mathrm{𝖺𝗉}}_{f^{-1}}(q){\beta }_{a^{\prime }}\right)$ $=\alpha _{f(a)}{}^{-1}{\alpha }_{f(a)}{\mathrm{𝖺𝗉}}_f\left(\beta _a{}^{-1}{\mathrm{𝖺𝗉}}_{f^{-1}}(q){\beta }_{a^{\prime }}\right)\alpha _{f(a^{\prime })}{}^{-1}{\alpha }_{f(a^{\prime })}$

$=\alpha _{f(a)}{}^{-1}{\mathrm{𝖺𝗉}}_f\left({\mathrm{𝖺𝗉}}_{f^{-1}}\left({\mathrm{𝖺𝗉}}_f\left(\beta _a{}^{-1}{\mathrm{𝖺𝗉}}_{f^{-1}}(q){\beta }_{a^{\prime }}\right)\right)\right){\alpha }_{f(a^{\prime })}$

$=\alpha _{f(a)}{}^{-1}{\mathrm{𝖺𝗉}}_f\left({\beta }_a\beta _a{}^{-1}{\mathrm{𝖺𝗉}}_{f^{-1}}(q){\beta }_{a^{\prime }}\beta _{a^{\prime }}{}^{-1}\right){\alpha }_{f(a^{\prime })}$

$=\alpha _{f(a)}{}^{-1}{\mathrm{𝖺𝗉}}_f({\mathrm{𝖺𝗉}}_{f^{-1}}(q)){\alpha }_{f(a^{\prime })}$

$=q.\mathit{∎}$

Thus, if for some type $A$ we have a full characterization of $a{=}_A{a}^{\prime }$, the type $p{=}_{a{=}_A{a}^{\prime }}q$ is determined as well. For example:

• Paths $p=q$, where $p,q:w{=}_{A\times B}{w}^{\prime }$, are equivalent to pairs of paths

  $${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}p{=}_{{\mathrm{𝗉𝗋}}_{1}w{=}_A{\mathrm{𝗉𝗋}}_1{w}^{\prime }}{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}q\mathit{\hspace{1em}}\text{and}\mathit{\hspace{1em}}{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}p{=}_{{\mathrm{𝗉𝗋}}_{2}w{=}_B{\mathrm{𝗉𝗋}}_2{w}^{\prime }}{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}q.$$

• Paths $p=q$, where $p,q:f{=}_{{\prod }_{(x:A)}B(x)}g$, are equivalent to homotopies

  $$\prod _{x:A}(\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(p)(x){=}_{f(x)=g(x)}\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}(q)(x)).$$

Next we consider transport in families of paths, i.e. transport in $C:A\to 𝒰$ 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\mathrm{:}A$, with $p\mathrm{:}{x}_{\mathrm{1}}\mathrm{=}{x}_{\mathrm{2}}$, we have

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto (a=x)}(p,q)$ $=qp$ for $q\mathrm{:}a\mathrm{=}{x}_{\mathrm{1}}$,

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto (x=a)}(p,q)$ $=p^{-1}q$ for $q\mathrm{:}{x}_{\mathrm{1}}\mathrm{=}a$,

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto (x=x)}(p,q)$ $=p^{-1}qp$ for $q\mathrm{:}{x}_{\mathrm{1}}\mathrm{=}{x}_{\mathrm{1}}$.

Proof.

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

In other words, transporting with $x\mapsto c=x$ is post-composition, and transporting with $x\mapsto x=c$ is contravariant pre-composition. These may be familiar as the functorial actions of the covariant and contravariant hom-functors $\mathrm{hom}(c,\text{–})$ and $\mathrm{hom}(\text{–},c)$ in category theory.

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\mathrm{,}g\mathrm{:}A\mathrm{\to }B$, with $p\mathrm{:}a{\mathrm{=}}_A{a}^{\mathrm{\prime }}$ and $q\mathrm{:}f\mathit{}\mathrm{(}a\mathrm{)}{\mathrm{=}}_{B}g\mathit{}\mathrm{(}a\mathrm{)}$, we have

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto f(x){=}_{B}g(x)}(p,q){=}_{f(a^{\prime })=g(a^{\prime })}{({\mathrm{𝖺𝗉}}_{f}p)}^{-1}q{\mathrm{𝖺𝗉}}_{g}p.$$

Because ${\mathrm{𝖺𝗉}}_{(x\mapsto x)}$ is the identity function and ${\mathrm{𝖺𝗉}}_{(x\mapsto c)}$ (where $c$ is a constant) is ${\mathrm{𝗋𝖾𝖿𝗅}}_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\mathrm{:}A\mathrm{\to }\mathrm{U}$ and $f\mathrm{,}g\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathit{}\mathrm{(}x\mathrm{)}$, with $p\mathrm{:}a{\mathrm{=}}_A{a}^{\mathrm{\prime }}$ and $q\mathrm{:}f\mathit{}\mathrm{(}a\mathrm{)}{\mathrm{=}}_{B\mathit{}\mathrm{(}a\mathrm{)}}g\mathit{}\mathrm{(}a\mathrm{)}$. Then we have

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto f(x){=}_{B(x)}g(x)}(p,q)={({\mathrm{𝖺𝗉𝖽}}_f(p))}^{-1}{\mathrm{𝖺𝗉}}_{({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{A}p)}(q){\mathrm{𝖺𝗉𝖽}}_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\mathrm{:}a{\mathrm{=}}_A{a}^{\mathrm{\prime }}$ with $q\mathrm{:}a\mathrm{=}a$ and $r\mathrm{:}{a}^{\mathrm{\prime }}\mathrm{=}{a}^{\mathrm{\prime }}$, we have

$$({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto (x=x)}(p,q)=r)\simeq (qp=pr).$$

Proof.

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