# 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)