"Locales and toposes as spaces": points

[anhinga_drafts]

I've completed the first reading of Steve Vickers' rather brilliant text, "Locales and toposes as spaces", from here

http://www.cs.bham.ac.uk/~sjv/

The problem with all these categorical games is that one can understand every neat trick separately, but there are just too many of them, and it's difficult to hold the resulting picture together. So I think I'll try to write them down, one trick at a time, and this might help me.

Trick of the day: points as arrows. If a category has a terminal object 1, then (global) points of object X are (defined as) arrows 1 → X. However, in many cases there are not enough global points, so for any object A people define "points of X at stage A" as arrows A → X. In particular, the "generic point" of X is simply the identity arrow, id : X → X.

Comments

[anhinga-drafts.livejournal.com]

I am asking, because there is a lot in common between modern functional programming and categories; the topic deserves a separate post.

Regarding your question, I think any knowledge tends to inform one's practices (in conventional mathematics, or conventional programming, respectively) and to be helpful. So the little snippets are quite useful.

But to be able to effectively work within the framework of categories (or within the framework of functional programming) one needs to practice. I think it's more a matter of practice and of getting really comfortable with the mindset, than a matter of accumulating knowledge.

And I can't say that I had enough practice or got sufficiently comfortable in either of these two fields. I think the factors preventing functional programming from being more popular in the industry and the factors preventing categories from being more popular among working mathematicians are similar.