Jonathan Cast <jonathanccast <at> fastmail.fm> writes: > > > > >>> 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe