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.