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

We introduce a primitive constant $c_{\mathrm{\Pi }}$, but write$c_{\mathrm{\Pi }}(A,\lambda x.B)$ as ${\prod }_{(x:A)}B$. Judgments concerningsuch expressions and expressions of the form $\lambda x.b$ are introduced by the following rules:

• if $\mathrm{\Gamma }⊢A:{𝒰}_n$ and $\mathrm{\Gamma },x:A⊢B:{𝒰}_n$, then $\mathrm{\Gamma }⊢{\prod }_{(x:A)}B:{𝒰}_n$

• if $\mathrm{\Gamma },x:A⊢b:B$ then $\mathrm{\Gamma }⊢(\lambda x.b):({\prod }_{(x:A)}B)$

• if $\mathrm{\Gamma }⊢g:{\prod }_{(x:A)}B$ and $\mathrm{\Gamma }⊢t:A$ then $\mathrm{\Gamma }⊢g(t):B[t/x]$

If $x$ does not occur freely in $B$, we abbreviate ${\prod }_{(x:A)}B$ as the non-dependent function type$A\to B$ and derive the following rule:

• if $\mathrm{\Gamma }⊢g:A\to B$ and $\mathrm{\Gamma }⊢t:A$ then $\mathrm{\Gamma }⊢g(t):B$

Using non-dependent function types and leaving implicit the context $\mathrm{\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:{𝒰}_n$ and $B:A\to {𝒰}_n$, then ${\prod }_{(x:A)}B(x):{𝒰}_n$

• if $x:A⊢b:B$ then $\lambda x.b:{\prod }_{(x:A)}B(x)$

• if $g:{\prod }_{(x:A)}B(x)$ and $t:A$ then $g(t):B(t)$