Let us begin by considering products of sets. Given sets A and B, the cartesian product of A and B is the set of ordered pairs

A × B = {(a, b)| a ∈ A, b ∈ B}

There are two coordinate projections:

with:

*fst ∘ (a, b) = a**snd ∘ (a, b) = b*

This notion of product relates to scala.Product, which is the base trait for all tuples and case classes.

For any element in *c ∈ A × B*, we have *c = (fst ∘ c, snd ∘ c)*

If we recall from day 15, we can generalize the concept of elements by introducing the singleton **1** explicitly.

If we clean it up a bit more, we get the following categorical definition of a product:

Definition 2.15.In any categoryC, a product diagram for the objects A and B consists of an object P and arrows p_{1}and p_{2}

satisfying the following UMP:Given any diagram of the form

there exists a unique u: X => P, making the diagram

commute, that is, such that x_{1}= p_{1}u and x_{2}= p_{2}u.

“There exists unique u” is a giveaway that this definition is an UMP.

If we step back to **Sets**, all it’s saying is that given type *A* and type *B*, there’s a unique function that can return `(A, B)`

. But how can we prove that for all categories? All we have at our disposal are alphabets and arrows.

Proposition 2.17Products are unique up to isomorphism.

Suppose we have *P* and *Q* that are products of objects *A* and *B*.

- Because
*P*is a product, there is a unique*i: P => Q*such that*p*and_{1}= q_{1}∘ i*p*_{2}= q_{2}∘ i - Because
*Q*is a product, there is a unique*j: Q => P*such that*q*and_{1}= p_{1}∘ j*q*_{2}= p_{2}∘ j - By composing
*j*and*i*we get*1*_{P}= j ∘ i - Similarly, we can also get
*1*_{Q}= i ∘ j - Thus
*i*is an isomorphism, and*P ≅ Q*∎

Since all products are isometric, we can just denote one as *A × B*, and the arrow *u: X => A × B* is denoted as *⟨x _{1}, x_{2}⟩*.

herding cats — Product