Screenshot from this video: https://www.youtube.com/watch?v=Bsdl_NKbNnU&index=8&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_
Bartosz was talking about the definition of product in category theory:
Let $c',c, a, b$ be objects in an category, and $p, q, p', q', m$ be arrows, such that:
- $p: c \rightarrow a$
- $q: c \rightarrow b$
- $p': c' \rightarrow a$
- $q': c' \rightarrow b$
- $m$ is the unique arrow from $c'$ to $c$
He went on to give an example in computer programming (where objects are types):
- $c$ is
(Int, Bool) - $c'$ is
(Int, Int, Bool) - $m$ is a function that takes the 1st and the 3rd elements of the tuple and returns a new tuple with them
- $p$ is a function that returns the first element of the tuple (an
Int). - $q$ is a function that returns the second element of the tuple (a
Bool). - $p'$ is a function that returns the first element of the tuple (an
Int). - $q'$ is a function that returns the third element of the tuple (a
Bool).
He then said that $c$ is "better" than $c'$ because of the extra step $m$. I am thinking, what if there is also an $m': c \rightarrow c'$? One can easily imagine a function that takes a (Int, Bool) and returns a (Int, Int, Bool), just put a 0 in between, for a trivial example. Could anyone help me understand this?
In your example, you can indeed imagine a map $c \to c'$ that commutes properly with $p,q,p',q'$ and inserts a $0$ in the middle. But you could also insert a $1$, or a $2$, or anything else.
Thus, in some sense, $c'$ contains some information that is completely irrelevant to the product.
On the flip side, the map $m : c' \to c$ that makes the diagram commute is unique; the condition that the composite maps $c' \xrightarrow{m} c \xrightarrow{p} a$ and $c' \xrightarrow{m} c \xrightarrow{q} b$ have to equal $p'$ and $q'$ completely determines what the map $c' \to c$ has to be.
This notion is actually one of the many ways to define the product: as an object $c$ together with a family of bijections $$ \eta_d : \hom(d, c) \cong \hom(d, a) \times \hom(d,b) $$ that is natural in $d$. (i.e. $\eta$ a natural isomorphism bewteen the two $\mathbf{Set}$-valued functors $\hom(-,c)$ and $\hom(-,a) \times \hom(-,b)$)