# A.2.4 Dependent function types ($\Pi$-types)

In §1.2 (http://planetmath.org/12functiontypes), we introduced non-dependent functions $A\to B$ in order to define a family of types as a function ${\lambda}(x\,{:}\,A).\,B:A\to\mathcal{U}_{i}$, which then gives rise to a type of dependent functions $\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}B$. But with explicit contexts we may replace ${\lambda}(x\,{:}\,A).\,B:A\to\mathcal{U}_{i}$ with the judgment

 $x\mathord{:}A\vdash B:\mathcal{U}_{i}.$

Consequently, we may define dependent functions directly, without reference to non-dependent ones. This way we follow the general principle that each type former, with its constants and rules, should be introduced independently of all other type formers. In fact, henceforth each type former is introduced systematically by:

For the dependent function type these rules are: {mathparpagebreakable} \inferrule*[right=$\Pi$-form] Γ ⊢A : $\mathcal{U}$ _i Γ,x : A ⊢B : $\mathcal{U}$ _iΓ ⊢∏_(x:A)B : $\mathcal{U}$ _i \inferrule*[right=$\Pi$-intro] Γ,x : A ⊢b : B Γ ⊢λ(x : A). b : ∏_(x:A)B \inferrule*[right=$\Pi$-elim] Γ ⊢f : ∏_(x:A)B
Γ ⊢a : A Γ ⊢f(a) : B[a/x] \inferrule*[right=$\Pi$-comp] Γ,x : A ⊢b : B
Γ ⊢a : A Γ ⊢(λ(x : A). b)(a) ≡b[a/x] : B[a/x] \inferrule*[right=$\Pi$-uniq] Γ ⊢f : ∏_(x:A)B Γ ⊢f ≡(λx. f(x)) : ∏_(x:A)B
The expression ${\lambda}(x\,{:}\,A).\,b$ binds free occurrences of $x$ in $b$, as does $\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}B$ for $B$.
When $x$ does not occur freely in $B$ so that $B$ does not depend on $A$, we obtain as a special case the ordinary function type $A\to B:\!\!\equiv\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{% (x:A)}}{\prod_{(x:A)}}B$. We take this as the definition of $\to$.
We may abbreviate an expression ${\lambda}(x\,{:}\,A).\,b$ as ${\lambda}x.\,b$, with the understanding that the omitted type $A$ should be filled in appropriately before type-checking.
Title A.2.4 Dependent function types ($\Pi$-types)