On Thursday 12 July 2007, Andrew Coppin wrote:
> Stefan O'Rear wrote:
> > On Thu, Jul 12, 2007 at 07:19:07PM +0100, Andrew Coppin wrote:
> >> I'm still puzzled as to what makes the other categories so magical that
> >> they cannot be considered sets.
> >>
> >> I'm also a little puzzled that a binary relation isn't considered to be
> >> a function...
> >>
> >> From the above, it seems that functors are in fact structure-preserving
> >> mappings somewhat like the various morphisms found in group theory. (I
> >> remember isomorphism and homomorphism, but there are really far too many
> >> morphisms to remember!)
> >
> > Many categories have more structure than just sets and functions. For
> > instance, in the category of groups, arrows must be homomorphisms.
>
> What the heck is an arrow when it's at home?
A homomorphism is just a function that preserves the group operation (addition
or multiplication, depending on the group); i.e., one that does what you
expect when presented with addition or multiplication (or whatever).
> > Some categories don't naturally correspond to sets - consider eg the
> > category of naturals, where there is a unique arrow from a to b iff a ≤
> > b.
>
> ...um...
Meditate on this at greater length. Here lies the path to enlightenment.
Incidentally, I think this lies behind the Curry-Howard isomorphism mentioned
earlier. In a category C, the product (a, b) of two objects is the triple
(p, p1 :: p -> a, p2 :: p -> b) such that for all triples (c, c1 :: c -> a,
c2 :: c -> b) there is precisely one arrow h :: c -> p such that p1 . h = c1
and p2 . h = c2. So, taking Prop to be the category of propositions such
that, for all propositions p, q, the pair (p, q) is an arrow from p to q iff
p => q, the product (p, q) is the proposition c such that c => p, c => q, and
for all propositions d such that d => p and d => q, d => c. Of course, c is
just p /\ q.
> > Binary relations are more general then functions, since they can be
> > partial and multiple-valued.
>
> What's a partial relation?
Let P, Q be sets, let r `subset` (P, Q) be a relation on P and Q, and for p
`elem` P, r(p) = { q `elem` Q | (p, q) `elem` r }. Then r is:
* total iff for all p `elem` P. r(p) contains at least one element,
* partial iff r is not total,
* a partial function iff for all p `elem` P. r(p) contains at most one
element,
* multi-valued iff r is not a partial function, and
* a function iff r is a partial function and total.
> > indeed, it is possible to form
> > the "category of small categories" with functors for arrows. ("Small"
> > means that there is a set of objects involved; eg Set is not small
> > because there is no set of all sets (see Russel's paradox) but Nat is
> > small.)
>
> OK, see, RIGHT THERE! That's the kind of sentence that I read and three
> of my cognative processes dump sort with an "unexpected out of neural
> capacity exception". o_O
I'd think you'd expect it by now :) Lessa answered this one competently
enough, I think.
Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
