Also see Pairs for newer supplementary material.

next up previous contents index
Next: Disjoint Union Up: Extending the Typed Previous: Cartesian Product

Dependent Products

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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995