Product type

Given types and , the product type contains ordered pairs for and , i.e. it generalizes the cartesian product. Under propositions as types, this corresponds to conjunction, since a proof of gives a proof of and a proof of .

Standard presentation

In the cartesian calculus of substitutions we can introduce product types with the following typing rules. The formation, introduction, and elimination rules are

while we also have the substitution naturality rules

and judgemental computation rules for β-computation and η-unicity

From -types

In the Cartesian calculus of substitutions with -types, it is not necessary to give separate typing rules to establish product types. Instead we have

and so we can define .

Derivation of above typing rules

For , we have

so we take .

For we have

so we take .

For we have

so we take .

The equalities follow.

#state/tidy | #lang/en | #SemBr