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.
