# A.1.3 Dependent pair types ($\Sigma$-types)

We introduce primitive constants $c_{\Sigma}$ and $c_{\mathsf{pair}}$. An expression of the form $c_{\Sigma}(A,{\lambda}a.\,B)$ is written as $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}B$, and an expression of the form $c_{\mathsf{pair}}(a,b)$ is written as $(a,b)$. We write $A\times B$ instead of $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B$ if $x$ is not free in $B$.

Judgments concerning such expressions are introduced by the following rules:

• if $A:\mathcal{U}_{n}$ and $B:A\rightarrow\mathcal{U}_{n}$, then $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x):\mathcal{U}_{n}$

• if, in addition  , $a:A$ and $b:B(a)$, then $(a,b):\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)$

If we have $A$ and $B$ as above, $C:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}% }{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:% A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{% (x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)\rightarrow\mathcal{U}_{m}$, and

 $d:\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{% (x:A)}}\mathchoice{{\textstyle\prod_{(y:B(x))}}}{\prod_{(y:B(x))}}{\prod_{(y:B% (x))}}{\prod_{(y:B(x))}}C((x,y))$

we can introduce a defined constant

 $f:\mathchoice{{\textstyle\prod_{(p:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x))}}}{\prod_{(p:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{% \prod_{(p:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum% _{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{\prod_{(p:\mathchoice{% \sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}% }{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:% A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{% (x:A)}}{\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},\ldots,x_{n}$ if they were obtained in some non-empty context; therefore, the fully explicit recursion schema is

 $f(x_{1},\dots,x_{n},(x(x_{1},\dots,x_{n}),y(x_{1},\dots,x_{n}))):\!\!\equiv d(% x_{1},\dots,x_{n},(x(x_{1},\dots,x_{n}),y(x_{1},\dots,x_{n}))).$
Title A.1.3 Dependent pair types ($\Sigma$-types)