() 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
On Tue, Sep 25, 2007 at 12:08:34AM -0500, Derek Elkins wrote: 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.)