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