Product Types
The binary product of two types is the set of ordered pairs of those two types. The values of the binary product is retrieved using projections, which select the first or second value in the pair. The nullary product (or unit) type consists of the empty tuple of no values.
More generally, the finite product type are tuples indexed by a finite set of indices. Special cases of the finite product type include:

ntuples where the indices i = {0, 1, …, n  1}

labelled tuples (or records) indexed by symbols
Products have both an eager and lazy interpretation.
The syntax for nullary and binary products is described by the following grammar:
Element  Abstract Syntax  Conrete Syntax  Description 

Typ t ::= 
unit 
unit 
nullary product 
prod(t1;t2) 
t1 X t2 
binary product 

Exp e ::= 
triv 
<> 
null tuple 
pair(e1;e2) 
<e1, e2> 
ordered pair 

pr [l] (e) 
e.l 
left projection 

pr [ r ] (e) 
e.r 
right projection 
Note that the type of the index is the dependent sum type where an integer index is bounded to 0 <= i < n. Where n = 0, the type of the index is empty, that is, it has no inhabitants. Writing the indices explicitly in the tuple:
(i.0 > t.0, i.1 > t.1, ..., i.n  1 > t.n  1)
makes clear the association between the index and the element. The indices can be represented as bounded integers or using unique labels so that the components of the tuple are more readable.
Product types are the essence of structured data. Common product types in programming languages includes:

functions with multiple arguments (a tuple with labels) or multiple results

objects represented as a set of functions

structues, labelled tuples with mutable data

arrays (a special tuple where the tuple has the same data type for each element)
Given the product type is fundamental to programming, it is suprising so many languages have so little support for them!