I have recently given Haskell another go, mostly because I heard about the book Haskell from first principles and so far I'm having a blast. My background is that of a mathematician mostly working in Algebra, so I usually understand the categorical aspects decently, but I could not quite grasp the following specific claim. On p.163 of Haskell from first principles, it is claimed that the functions
fst :: (a,b) -> a snd :: (a,b) -> b
are uniquely determined by their type signature.
Now, I feel like this is not true without some further naturality, compatibility or universality requirements that uniquely determine the explicit realisations of fst and snd given bindings of a and b to explicit types.
So my question is: What properties are fst and snd assumed to possess that indeed determine them uniquely?
I feel like I got a rough handwavy understanding of what is meant. If we want fst and snd to somehow "behave the same way" no matter which types we choose for a and b, then it feels like we indeed have no other choice but given an inhabitant of (a,b) return its constituents. However, I don't know what precisely is meant here.
At first glance, it might remind one of the categorical product in the category of sets, but the product already comes together with its two projection maps. Now of course we could say "fst and snd are already uniquely determined if we want the triple ( (a,b), fst, snd) ) to satisfy an analogon of the universal property of the categorical product", but that is a rather weak claim and certainly not what is said in the book.
Another idea is that maybe we want fst and snd to be compatible with maps in the sense that if
f :: a -> b is any function, then we might want something like
f a = fst.(f -*- id ) (a,undefined) to hold. (Or maybe undefined instead of id as well, but that shouldnt matter since we discard it anyway).
Any help is appreciated!