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:

•

a formation rule, stating when the type former can be applied;
•

some introduction rules, stating how to inhabit the type;
•

elimination rules, or an induction principle, stating how to use an element of the type;
•

computation rules, which are judgmental equalities explaining what happens when elimination rules are applied to results of introduction rules;
•

optional uniqueness principles, which are judgmental equalities explaining how every element of the type is uniquely determined by the results of elimination rules applied to it.

(See also \autorefrmk:introducing-new-concepts.)

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)
\metatable

A.2.4 Dependent function types (Π-types)

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