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.