
Jonathan Cast
Extensionality is a key part of the definition of all of these constructions. The categorical rules are designed to require, in concrete categories, that the range of the two injections into a coproduct form a partition of the coproduct, the surjective pairing law (fst x, snd x) = x holds, and the eta reduction law (\ x -> f x) = f holds. Haskell flaunts all three; while some categories have few enough morphisms to get away with this (at least some times), Hask is not one of them.
That interpretation is not something that is essential in the notion of category, only in certain specific examples of categories that you know.
I understand category theory. I also know that the definitions used are chosen to get Set `right', which means extensionality in that case, and are then extended uniformly across all categories. This has the effect of requiring similar constructions to those in Set in other concrete categories.
Referring to my copy of "Sheaves in Geometry and Logic", Moerdijk and Mac Lane state that "in 1963 Lawvere embarked on the daring project of a purely categorical foundation of all mathematics". Did he fail? I'm probably misunderstanding what you are saying here but I didn't think you needed sets to define categories; in fact Set is a topos which has far more structure than a category. Can you be clearer what you mean by extensionality in this context? And how it relates to Set? On a broader note, I'm pleased that this discussion is taking place and I wish someone would actually write a wiki page on why Haskell isn't a nicely behaved category and what problems this causes / doesn't cause. I wish I had time. Dominic.