Why definition of categorical product works for $C'=$(Int, Int, Bool) and $C=($Int, Bool$)$?

Question

In milewski-ctfp

is said that one can convert pseudo-product C' = (Int, Int, Bool) to product C = (Int, Bool) using function m that is uniquely determined as

m (x, _, b) = (x, b)

But there are two ways to define m

m (x, _, b) = (x, b)
m (_, x, b) = (x, b)

They are not equal, then m is not unique, then (int, bool) is not a product

Can you point where I'm wrong?

---

P.S. this is duplicate of issue https://github.com/hmemcpy/milewski-ctfp-pdf/issues/127

---

Update

image part 1

image part 2

Answer 1

(Int, Bool) together with p :: (Int, Bool) -> Int and q :: (Int, Bool) -> Bool given by the two projections is indeed a product of Int and Bool.

Recall that a product of two objects a and b is given by an object c together with two functions p :: c -> a, q :: c -> b such that for any other object c' and functions p' :: c' -> a, q' :: c' -> b there is a unique function m :: c' -> c such that p' = p . m, q' = q . m.

This last bit is important: there can be many functions m' :: c' -> c, but only one of them shall satisfy both p' = p . m' and q' = q . m'.

Let c' = (Int, Int, Bool) and p' :: (Int, Int, Bool) -> Int, q' :: (Int, Int, Bool) -> Bool with p' (x, _, _) = x and q' (_, _, b) = b.

If you define m :: c' -> c by m (_, x, b) = (x, b), then you have that p' (x, y, b) = x but p (m (x, y, b)) = p (y, b) = y, and so p' = p . m does not hold.

Therefore, it is true that there are two ways to define m :: c' -> c – actually, there are even more! We could also have m (x, _, _) = (x, True), or m (_, _, b) = (0, b), ... but of all these functions there is only one that satisfies p' = p . m, q' = q . m. This is what makes (Int, Bool) together with p :: (Int, Bool) -> Int and q :: (Int, Bool) -> Bool a product of Int and Bool.

Answer 2

If I interprete the notation correctly, we are given

$$\begin{align}p\colon \text{(Int, Int, Bool)}&\to \text{Int}\\(x,y,z)&\mapsto x\\ q\colon \text{(Int, Int, Bool)}&\to \text{Bool}\\(x,y,b)&\mapsto b\end{align}$$ and are looking for $m\colon\text{(Int, Int, Bool)}\to\text{(Int, Bool)} $ such that $\text{fst}\circ m=p$ and $\text{snd}\circ m=q$. If we want to compute $m(x,y,z)$, the result will certainly be of the form $(u,v)$ with $u\in\text{Int}$ and $v\in\text{Bool}$. From $$u=\text{fst}(u,v)=\text{fst}(m(x,y,z))=(\text{fst}\circ m)(x,y,z)=p(x,y,z)=x$$ $$v=\text{snd}(u,v)=\text{snd}(m(x,y,z))=(\text{snd}\circ m)(x,y,z)=q(x,y,z)=z$$ we conclude that $m(x,y,z)=(u,v)=(x,z)$, as stated in the text.

---

Remark: It seems you instead skimmed over a different bug in the text:

For instance, there is a
Boolean-valued function (a predicate) defined for every type:

\begin{Verbatim}
yes :: a -> Bool
yes _ = True
\end{Verbatim}
But \code{Bool} is not a terminal object. There is at least one more
\code{Bool}-valued function from every type:

\begin{Verbatim}
no :: a -> Bool
no _ = False
\end{Verbatim}

The point is that for the second function is in general not different from the first function (and so not "one more"). For (exhaustive) example, if a happens to be Void, both yes and no are the same, absurd.