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 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;
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 a
category. Can you be clearer what you mean by extensionality in
this 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
