Cartesian products

If A and B are types, then so is their product, written $A \times B$. There will be many formation rules of this form, so we adopt a simple convention for stating them. We write

$$\frac{A \mbox{is a} Type, B \mbox{is a} Type}{A \times B \ \mbox{is a} Type .}$$

The elements of a product are pairs, <a, b>. Specifically if a belongs to A and b belongs to B, then <a, b> belongs to $A \times B$. We abbreviate this by writing

$$\frac{a \epsilon A, b \epsilon B}{<a,b\gt \epsilon A \times B.}$$

In programming languages these types are generalized to n-ary products, say $A_1\times A_2\times \ldots\times A_n$ and called structures or records.

We say that <a,b> = <c,d> in $A \times B$ iff a=c in A and b=d in B.

In set theory, equality is uniform, but in type theory we define equality with each constructor.

There is essentially only one way to decompose pairs. We say things like, ``take the first element of the pair P,'' symbolically we might say first(P) or $1o\!f(P)$. We can also ``take the second element of P,'' second(P) or $2o\!f(P)$.