Also see Pairs for newer supplementary material.

Just as the function space constructor is generalized
from to , so too can the product
constructor be generalized to , where **B**
can depend on **x**.
For example, given the declarations
and , is a type in .
The formation rule for dependent types becomes the following.

The introduction rules change as follows.

The term ``over '' is needed in order to specify the substitution
of in **T**.

Thu Sep 14 08:45:18 EDT 1995