On 6 Jan 2008, at 12:27 PM, Dominic Steinitz wrote:

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 acoproduct form a partition of the coproduct, the surjectivepairinglaw (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", Moerdijkand Mac Lanestate that "in 1963 Lawvere embarked on the daring project of a purely categorical foundation of all mathematics". Did he fail? I'm probablymisunderstanding what you are saying here but I didn't think youneeded sets todefine categories;

`Right. But category theory is nevertheless `backward compatible'`

`with set theory, in the sense that the category theoretic`

`constructions in a category satisfying ZFC will be the same`

`constructions we are familiar with already. The category-theoretic`

`definitions, when specialized to Set, are precise (up to natural`

`isomorphism) definitions of the pre-existing concepts of cartesian`

`products, functions, etc. in Set. Or, to put it another way, the`

`category-theoretic definitions are generalizations of those pre-`

`existing concepts to other categories. Hask has a structure that is`

`Set-like enough that these concepts generalize very little when`

`moving to Hask.`

in fact Set is a topos which has far more structure than acategory. Can you be clearer what you mean by extensionality inthis context?

`By `extensionality' I mean the equalities which follow from using`

`standard set-theoretic definitions for functions, products,`

`coproducts, etc. --- surjective pairing, eta-contraction, etc. My`

`understanding is that, in fact, the category-theoretic definitions`

`are designed to capture those equations in diagrams that can be used`

`as definitions in arbitrary categories. It's possible to view those`

`definitions, then, as more fundamental descriptions of the concepts`

`than what they generalize, but the fact that they are generalizations`

`of the ideas from Set shows up in categories similar to Set (and Hask`

`is certainly more similar to Set than, say, Vec).`

jcc _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe