# A.1.8 Identity types

We introduce primitive constants $c_{=}$ and $c_{\mathsf{refl}}$. We write $a=_{A}b$ for $c_{=}(A,a,b)$ and $\mathsf{refl}_{a}$ for $c_{\mathsf{refl}}(A,a)$, when $a:A$ is understood:

• If $A:\mathcal{U}_{n}$, $a:A$, and $b:A$ then $a=_{A}b:\mathcal{U}_{n}$.

• If $a:A$ then $\mathsf{refl}_{a}:a=_{A}a$.

Given $a:A$, if $y:A,z:a=_{A}y\vdash C:\mathcal{U}_{m}$ and $\vdash d:C[a,\mathsf{refl}_{a}/y,z]$ then we can introduce a defined constant

 $f:\mathchoice{{\textstyle\prod_{(y:A)}}}{\prod_{(y:A)}}{\prod_{(y:A)}}{\prod_{% (y:A)}}\mathchoice{{\textstyle\prod_{(z:a=_{A}y)}}}{\prod_{(z:a=_{A}y)}}{\prod% _{(z:a=_{A}y)}}{\prod_{(z:a=_{A}y)}}C$

with defining equation

 $f(a,\mathsf{refl}_{a}):\!\!\equiv d.$
Title A.1.8 Identity types
\metatable