On Tue, Sep 25, 2007 at 12:08:34AM -0500, Derek Elkins wrote:
> () is terminal, not initial.  There exists a unique function to it
> (ignoring bottoms) from anything, namely, const ().  A "point" of A
> categorically, is just a function from the terminal object to A, () ->
> A.  For the notion of "pointed" that you want, the important thing is
> that f = g :: A -> B iff for all k :: () -> A, f . k = g . k.  I.e. a
> function is completely determined by its action on points.
Ah, a lightbulb clicked with this one. Since functions are objects in
this category, and we can't talk about function application 'cause
that'd be breaking the object-bubble, we establish equivalency between
function application and composition of a function with a point.
Presumably, a proof is in order.

(Sorry, feel free to ignore. Just a newb trying to catch up and convince
himself he's not totally whacked.)
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to