A.1.2 Dependent function types ( $\Pi$ -types)

We introduce a primitive constant $c_{\Pi}$ , but write $c_{\Pi}(A,{\lambda}x.\,B)$ as $\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}B$ . Judgments concerning such expressions and expressions of the form ${\lambda}x.\,b$ are introduced by the following rules:

•

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

if $\Gamma,x:A\vdash b:B$ then $\Gamma\vdash({\lambda}x.\,b):(\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x% :A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}B)$
•

if $\Gamma\vdash g:\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x% :A)}}{\prod_{(x:A)}}B$ and $\Gamma\vdash t:A$ then $\Gamma\vdash g(t):B[t/x]$

If $x$ does not occur freely in $B$ , we abbreviate $\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}B$ as the non-dependent function type $A\rightarrow B$ and derive the following rule:

•

if $\Gamma\vdash g:A\rightarrow B$ and $\Gamma\vdash t:A$ then $\Gamma\vdash g(t):B$

Using non-dependent function types and leaving implicit the context $\Gamma$ , the rules above can be written in the following alternative style that we use in the rest of this section of the appendix.

•

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

if $x:A\vdash b:B$ then ${\lambda}x.\,b:\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x% :A)}}{\prod_{(x:A)}}B(x)$
•

if $g:\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{% (x:A)}}B(x)$ and $t : A$ then $g(t):B(t)$

Title	A.1.2 Dependent function types ( $\Pi$ -types)
\metatable

A.1.2 Dependent function types (Π-types)

A.1.2 Dependent function types ( $\Pi$ -types)