The product, by its maps

The product $A \times B$ comes with two projections, $\pi_1(a, b) = a$ and $\pi_2(a, b) = b$. Given any set $Z$ and any functions $f : Z \to A$ and $g : Z \to B$, there is a function

with $\pi_1 \circ \langle f, g \rangle = f$ and $\pi_2 \circ \langle f, g \rangle = g$. The experiment shows more: it is the only such function. Any $h$ with $\pi_1 \circ h = f$ and $\pi_2 \circ h = g$ must send $z$ to the pair with first coordinate $f(z)$ and second coordinate $g(z)$ — that is, $h = \langle f, g \rangle$.

/-- Following `pair f g` by the first projection gives back `f`. -/
theorem fst_comp_pair (f : Z → A) (g : Z → B) : Prod.fst ∘ pair f g = f := rfl

/-- **Universal property of the product, uniqueness half.** Any `h : Z → A × B` whose two
coordinates are `f` and `g` *is* `pair f g`. Together with `fst_comp_pair` and
`snd_comp_pair` (existence), this says: maps into `A × B` are the same thing as pairs of
maps into `A` and into `B`. -/
theorem pair_unique {f : Z → A} {g : Z → B} (h : Z → A × B)
    (hf : Prod.fst ∘ h = f) (hg : Prod.snd ∘ h = g) : h = pair f g := by
  funext z
  show h z = (f z, g z)
  rw [← hf, ← hg]
  -- The goal is now `h z = ((h z).1, (h z).2)`: every pair is built from its coordinates.
  rfl

This "exists and is unique" statement is called the universal property of the product. It describes $A \times B$ entirely through its relationships with all other sets, without mentioning ordered pairs at all. In any category, an object with two arrows satisfying this property is called a product of $A$ and $B$.

The universal property pins the product down up to isomorphism: any two products of $A$ and $B$ are related by a unique isomorphism compatible with the projections — though they need not be literally equal. In the category of subsets of a set ordered by $\subseteq$, the product of $A$ and $B$ turns out to be $A \cap B$; in other categories products look different again. Universal properties like this one are the starting point for limits, adjunctions and the Yoneda lemma.