"Locales and toposes as spaces": categories as theories

[anhinga_drafts]

I am continuing the last three postings in this blog, and jumping to Section 5.3 of Vickers' text.

One can take a category and interpret it as a predicate theory. All objects A are interpreted as sorts, X_A, and all arrows f : A → B are interpreted as functional symbols, u_f : X_A → X_B.

Then for every object A one imposes an axiom (∀x:X_A) u_idA (x) = x.

And for every pair of morphisms f : A → B, g : B → C one considers the morphism h = g o f and imposes an axiom (∀x:X_A) u_g (u_f (x)) = u_h (x).

One often imposes additional axioms as well. Of course, this is a lot of sorts, functional symbols, and axioms. If one at least wants them to form sets rather than proper classes, one has to start with a small category.

Also we can't assume that objects are sets which have elements, so what would (∀x:X_A) even mean? One can think about this purely formally (until one starts to consider models of the theories), or one can recall from a first post in this series than a generalized point of A is simply a morphism x to A, then f (x) should be thought of as f o x, and one can think about quantifiers ranging over these generalized points.

Comments

[http://users.livejournal.com/_rowan_tree_/]

So that the your friends are included. ./*/* doesn't include ./* :-)

[anhinga-anhinga.livejournal.com]

Well, this seems to be quite orthogonal to filtering -- this is just about inability to merge F and FOF.

In any case, the filtering of F by tags does not seem to work :-(

[http://users.livejournal.com/_rowan_tree_/]

I was wrong on the first one then :-(
We need full algebra there: (F \cup FOF) select tags = t1 or t2 or t3
Not in our lifetime, I suppose :-(

[anhinga-anhinga.livejournal.com]

Yes, the question is how to give users the full algebra (of stream-related operations in general), but to keep them from overloading servers.

Not at LiveJournal, I suppose, given its corporate mindset, but, perhaps, elsewhere..