Product 

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:
coordinate projections

with:

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.

product of sets

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

Definition 2.15. In any category C, a product diagram for the objects A and B consists of an object P and arrows p1 and p2
product diagram
satisfying the following UMP:

Given any diagram of the form
product definition
there exists a unique u: X => P, making the diagram
product of objects
commute, that is, such that x1 = p1 u and x2 = p2 u.

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

Uniqueness of products 

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.17 Products are unique up to isomorphism.

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

uniqueness of products

  1. Because P is a product, there is a unique i: P => Q such that p1 = q1 ∘ i and p2 = q2 ∘ i
  2. Because Q is a product, there is a unique j: Q => P such that q1 = p1 ∘ j and q2 = p2 ∘ j
  3. By composing j and i we get 1P = j ∘ i
  4. Similarly, we can also get 1Q = i ∘ j
  5. 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 ⟨x1, x2.