A.1.3 Dependent pair types ($\mathrm{\Sigma }$-types)

We introduce primitive constants $c_{\mathrm{\Sigma }}$ and $c_{\mathrm{𝗉𝖺𝗂𝗋}}$. An expression of the form $c_{\mathrm{\Sigma }}(A,\lambda a.B)$ is written as ${\sum }_{(a:A)}B$, and an expression of the form $c_{\mathrm{𝗉𝖺𝗂𝗋}}(a,b)$ is written as $(a,b)$. We write $A\times B$ instead of ${\sum }_{(x:A)}B$ if $x$ is not free in $B$.

Judgments concerning such expressions are introduced by the following rules:

• if $A:{𝒰}_n$ and $B:A\to {𝒰}_n$, then ${\sum }_{(x:A)}B(x):{𝒰}_n$

• if, in addition, $a:A$ and $b:B(a)$, then $(a,b):{\sum }_{(x:A)}B(x)$

If we have $A$ and $B$ as above, $C:{\sum }_{(x:A)}B(x)\to {𝒰}_m$, and

$$d:{\prod }_{(x:A)}{\prod }_{(y:B(x))}C((x,y))$$

we can introduce a defined constant

$$f:{\prod }_{(p:{\sum }_{(x:A)}B(x))}C(p)$$

with the defining equation

$$f((x,y)):\equiv d(x,y).$$

Note that $C$, $d$, $x$, and $y$ may contain extra implicit parameters $x_1,\mathrm{\dots },x_n$ if they were obtained in some non-empty context; therefore, the fully explicit recursion schema is

$$f(x_1,\mathrm{\dots },x_n,(x(x_1,\mathrm{\dots },x_n),y(x_1,\mathrm{\dots },x_n))):\equiv d(x_1,\mathrm{\dots },x_n,(x(x_1,\mathrm{\dots },x_n),y(x_1,\mathrm{\dots },x_n))).$$

Title	A.1.3 Dependent pair types ($\mathrm{\Sigma }$-types)