[Haskell-cafe] Re: Basic question concerning the category Hask (was: concerning data constructors)

[Dominic Steinitz]

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.