# 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:A\to B$ is an equivalence, then for all $a,a^{\prime}:A$, so is

 $\mathsf{ap}_{f}:(a=_{A}a^{\prime})\to(f(a)=_{B}f(a^{\prime})).$
###### Proof.

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

 $\alpha:\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod% _{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}% }{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{% (b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}(f(\mathord{{f}^{-1}}(b)% )=b)\qquad\text{and}\qquad\beta:\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)}}}(\mathord{{f}^{-1}}(f(a))=a).$

The quasi-inverse of $\mathsf{ap}_{f}$ is, essentially,

 $\mathsf{ap}_{\mathord{{f}^{-1}}}:(f(a)=f(a^{\prime}))\to(\mathord{{f}^{-1}}(f(% a))=\mathord{{f}^{-1}}(f(a^{\prime}))).$

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

 $\mathord{{\beta_{a}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{\mathord{{f}^{-1}}}% (\mathsf{ap}_{f}(p))\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\beta_{a^{\prime}}=p.$

This follows from the functoriality of $\mathsf{ap}$ 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

 $\mathsf{ap}_{f}\big{(}\mathord{{\beta_{a}}^{-1}}\mathchoice{\mathbin{\raisebox% {2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}% }}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{\mathord{{% f}^{-1}}}(q)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}% }{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\beta_{a^{\prime}}\big{)}=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):

 $\displaystyle\mathsf{ap}_{f}\big{(}\mathord{{\beta_{a}}^{-1}}\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}% _{\mathord{{f}^{-1}}}(q)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\beta_{a^{\prime}}\big{)}$ $\displaystyle=\mathord{{\alpha_{f(a)}}^{-1}}\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}{\alpha_{f(a)}}\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}% _{f}\big{(}\mathord{{\beta_{a}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{\mathord{{f}^{-1}}}% (q)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\beta_{a^{\prime}}\big{)}\mathchoice{\mathbin{\raisebox{2.15% pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{\alpha_{f(a^{\prime})}% }^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}{\alpha_{f(a^{\prime})}}$ $\displaystyle=\mathord{{\alpha_{f(a)}}^{-1}}\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f}\big{(}\mathsf{ap% }_{\mathord{{f}^{-1}}}\big{(}\mathsf{ap}_{f}\big{(}\mathord{{\beta_{a}}^{-1}}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathsf{ap}_{\mathord{{f}^{-1}}}(q)\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\beta_{a^{\prime}}\big{)}\big{)}% \big{)}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}{\alpha_{f(a^{\prime})}}$ $\displaystyle=\mathord{{\alpha_{f(a)}}^{-1}}\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f}\big{(}\beta_{a}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathord{{\beta_{a}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{\mathord{{f}^{-1}}}% (q)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\beta_{a^{\prime}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{\beta_{a^{\prime}}}^{-% 1}}\big{)}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}{\alpha_{f(a^{\prime})}}$ $\displaystyle=\mathord{{\alpha_{f(a)}}^{-1}}\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f}(\mathsf{ap}_{% \mathord{{f}^{-1}}}(q))\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}{\alpha_{f(a^{\prime})}}$ $\displaystyle=q.\qed$

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

 $\mathsf{ap}_{\mathsf{pr}_{1}}{p}=_{\mathsf{pr}_{1}w=_{A}\mathsf{pr}_{1}w^{% \prime}}\mathsf{ap}_{\mathsf{pr}_{1}}{q}\quad\text{and}\quad\mathsf{ap}_{% \mathsf{pr}_{2}}{p}=_{\mathsf{pr}_{2}w=_{B}\mathsf{pr}_{2}w^{\prime}}\mathsf{% ap}_{\mathsf{pr}_{2}}{q}.$
• Paths $p=q$, where $p,q:f=_{\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)}g$, are equivalent to homotopies

 $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(\mathsf{happly}(p)(x)=_{f(x)=g% (x)}\mathsf{happly}(q)(x)).$

Next we consider transport in families of paths, i.e. transport in $C:A\to\mathcal{U}$ 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:x_{1}=x_{2}$, we have

 $\displaystyle\mathsf{transport}^{x\mapsto(a=x)}(p,q)$ $\displaystyle=q\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot% }}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}p$ for $q:a=x_{1}$, $\displaystyle\mathsf{transport}^{x\mapsto(x=a)}(p,q)$ $\displaystyle=\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q$ for $q:x_{1}=a$, $\displaystyle\mathsf{transport}^{x\mapsto(x=x)}(p,q)$ $\displaystyle=\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q\mathchoice{\mathbin{\raisebox{% 2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}% }{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p$ for $q:x_{1}=x_{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 $\hom(c,{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})$ and $\hom({\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}},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,g:A\to B$, with $p:a=_{A}a^{\prime}$ and $q:f(a)=_{B}g(a)$, we have

 $\mathsf{transport}^{x\mapsto f(x)=_{B}g(x)}(p,q)=_{f(a^{\prime})=g(a^{\prime})% }\mathord{{(\mathsf{ap}_{f}{p})}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q\mathchoice{\mathbin{\raisebox{% 2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}% }{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{g}{p}.$

Because $\mathsf{ap}_{(x\mapsto x)}$ is the identity function and $\mathsf{ap}_{(x\mapsto c)}$ (where $c$ is a constant) is $\mathsf{refl}_{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:A\to\mathcal{U}$ and $f,g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$, with $p:a=_{A}a^{\prime}$ and $q:f(a)=_{B(a)}g(a)$. Then we have

 $\mathsf{transport}^{x\mapsto f(x)=_{B(x)}g(x)}(p,q)=\mathord{{(\mathsf{apd}_{f% }(p))}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}% }{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\mathsf{ap}_{(\mathsf{transport}^{A}{p})}(q)\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{apd% }_{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=_{A}a^{\prime}$ with $q:a=a$ and $r:a^{\prime}=a^{\prime}$, we have

 $\big{(}\mathsf{transport}^{x\mapsto(x=x)}(p,q)=r\big{)}\;\simeq\;\big{(}q% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}p=p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}r\big{)}.$
###### Proof.

Path induction on $p$, followed by the fact that composing with the unit equalities $q\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}1=q$ and $r=1\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}r$ 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