I'm working through Bartosz Milewski's awesome blogs about category theory. I'm stuck on the one on products and coproducts.
Bartosz says that a product of two objects a and b is the object c equipped with two projections such that for any other object c' equipped with two projections there is a unique morphism m from c' to c that factorizes those projections.
Of course we can find a suitable example in the category of sets and functions. The product of two types Int and Bool is the pair (Int, Bool). The two projections are p (int, _) = int and q (_, bool) = bool. There is, however, another candidate for the product of Int and Bool: it is the type Int with projections p' int = int and q' _ = True. As Bartosz says: "That’s pretty lame, but it matches the criteria." Notice that the product type Int contains less values than the product type (Int, Bool). Half as much, to be precise. Even though both product types can be mapped to the entire Int type, the product type Int can be mapped to only half of the Bool type. It is not surjective (if that is the right word for it)!
Because we can come up with a mormphism m :: (Int, Bool) -> Int (where m can only be uniquely implemented as m (int, _) = int) we know that the product type (Int, Bool) is better than Int. At this point I wonder: couldn't we just as easily implement m as m (int, _) = int + 1? Isn't that a second morphism that works? Or is that not allowed because the resulting product Int is actually not Int at all, but Int "shifted" by 1?
L
The arrow in your m points in the wrong direction. We know that (Int, Bool) is "better" than Int because we have a morphism m :: Int -> (Int, Bool), m x = (x, True). It satisfies the conditions p . m == p' and q . m == q', that's what is meant by m factorizing p' and q'. If you define m in any other way, this condition will not hold.
For example, if it was defined as m x = (x + 1, True), then p (m 0) == 1, but p' 0 == 0.
Your map m' :: (Int, Bool) -> Int, if it factorized p and q, would point to Int being a suitable product, too. But the composition q' . m' :: (Int, Bool) -> Bool always returns True, so it cannot be equal to q.