"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_/]

As an improvement to the public service, how about adding tags to these posts?

[anhinga-anhinga.livejournal.com]

Yes, I should really go over my blogs and add tags..

BTW, is there any way to see the set of all tags used in a particular LJ (or does the author need to explicitly list them for this), and is there any way to get postings from multiple blogs by a tag (for example, by filtering a friends page by a tag)?

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

I have no practical experience with tags :-(
Intuitively the answer to your second question should be "yes", and it's easy to try by the URL.
As for teh first, I seem to recall seeing something somewhere about this - try RTFM?

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

Filtering FOF page assumes reflexivity of "friends", BTW ;-)

[anhinga-anhinga.livejournal.com]

RTFM actually helps:

http://users.livejournal.com/_rowan_tree_/tag/

[anhinga-anhinga.livejournal.com]

Why?

[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..