Dear Andrej, I can offer a couple of thoughts, one simple and the other deeper but speculative. Note Andre's remark: it's not bounded linear orders that are classified by simplicial sets, but distinctly bounded linear orders (i.e. the bounds are distinct). The simple thought is that bounded linear orders are exactly lattices (necessarily distributive) satisfying the axiom x \/ y = x or x \/ y = y This gives a geometric theory Morita equivalent to that of bounded (distinctly bounded, if necessary) linear orders. The reason that's not completely uninteresting is because of the way the simplicial sets classify. You would expect (distinctly) bounded linear orders to be classified by the topos of _co_variant functors from the category of finite (distinctly) bounded linear orders to Set, and in fact this is the case. (Finite here = isomorphic to a finite cardinal.) But the category of finite distinctly bounded linear orders is dual to the simplicial category Delta, which gives the desired result. The duality is essentially a restriction of that between finite posets and finite distributive lattices, but the distributive lattices in this case are linear. (I discussed this issue in my paper "Strongly algebraic = SFP (topically)", where I developed some sufficient conditions for a classifying topos to be a presheaf topos, in situations like this where the finitely presentable models are finite.) Here are the deeper speculations. There's a series of dualities between discrete structures and Stone structures. (1) Discrete Boolean algebras dual to Stone objects (from the original Stone duality) (2) Discrete distributive lattices dual to Stone posets (from Priestley duality) (3) Discrete semilattices dual to Stone semilattices (4) Discrete posets dual to Stone distributive lattices (5) Discrete objects (sets) dual to Stone Boolean algebras These are all in "Stone Spaces" - sections II.4 and VI.3. These dualities become equivalences if you replace the structured Stone objects on the right by costructured Boolean algebras. I would conjecture that one can write down geometric theories for the costructured Boolean algebras on the right, Morita equivalent to those for the structured sets on the left. In fact, the last time I saw Japie Vermeulen he said he thought it was known, but he didn't show me any proof then and I haven't seen any since. (The context was that we were discussing the idea of representing a topos not, in the usual manner, by its category of discrete spaces - sheaves - but by its category of Stone spaces - dual to sheaves of Boolean algebras. A suitable constructive version of duality (5) would show that the sheaves can be recovered from the Stone space.) Since the distinctly bounded linear orders fit within the left hand side of the series of dualities, the conjecture would suggest there's a Morita equivalent theory of costructured Boolean algebras. All the best, Steve. On 31 Jul 2010, at 08:55, Andrej Bauer wrote:

The presheaf category of simplicial sets is the classifying topos for the theory L of a bounded linear order.

In general, there could be other theories which are "Morita equivalent" to L in the sense that their classifying toposes are equivalent to simplicial sets. Are any such known, preferably occurring in nature?

With kind regards,

Andrej

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Question to the list: I am very much interested, does there exist any practically usable system for the "computer algebra style" work with diagrams. I.e. not just write down the diagrams (like XyPic) but for example for diagram chasing, verification of commutativity in any interesting classes of categories with structure etc. As I remember there were some systems permitting computation of some limits in very limited classes of categories, also some heavy attempts of formalisation in some general purpose proof assistants but I do not know about anything else. Regards to all Sergei Soloviev [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

I paste and copy some old posting to this list that I have kept. It seems to me that they are relevant for your discussion. e.d.

I'd like to announce a selection of Web-based category theory demonstrations that I've put up at http://www.j-paine.org/cgi-bin/webcats/webcats.php . The page contains a number of buttons such as "generate and demonstrate an equaliser" and "generate and demonstrate a limit": clicking on one will generate an example of the construct in the category of finite sets, and display it as a listing of its objects and arrows, and as a diagram. For limits and colimits, the demos generate a small random graph, convert it to a diagram, then compute and display its limit or colimit.

Comments would be very welcome. The demos are a bit of an experiment: I had some categorical algorithms lying around from other work, and thought it would be interesting to connect them to the Web.

"If you could commission a computer demonstration of any categorical idea, what would you ask for? Could such demonstrations have helped you, or your students, learn tricky ideas? And, would you be willing to share the visualisations and metaphors that you have devised to explain these ideas to yourself or others?"

We've started a thread on this topic at the n-Category Cafe', http://golem.ph.utexas.edu/category/2009/04/graphical_category_theory_demo.h... . Anybody interested in using computers to demonstrate concepts from category theory, do please have a look there. I've just added an explanation of the techniques available for delivering demonstrations over the Web, and I mention one - the 3D modelling environment called Alice - that I think will eventually be brilliant for animating category theory, and many other topics besides.

This is to tell, or remind, readers about the Web-based interactive category-theory demonstrations I have on my site. Perhaps of interest to new students now an academic year is starting. They're at http://www.j-paine.org/cgi-bin/webcats/webcats.php . After some preamble, this page contains a form divided into sections. Each section generates a particular construct in the category of finite sets: e.g. a colimit, equaliser, or initial object. You can input sets and arrows, or let the demo choose its own. The output includes a diagram, and text explaining it.

Cheers,

Jocelyn Paine http://www.j-paine.org +44 (0)7768 534 091

Jocelyn's Cartoons: http://www.j-paine.org/blog/jocelyns_cartoons/

On 03/10/11 15:02, Michael J Healy wrote:

Sergei,

My colleagues and I have been looking for something like this for a project. We need to be able to specify small categories as the completions of finite graphs we are given, extend these by specifying commutative diagrams, pullbacks, etc, of interest, then define functors generated from graph homomorphisms, and take colimits of diagrams in Cat, etc etc. We haven't found anything that does all this. So, we're programming it in Haskell---one of our grad students knows the language. We'll be happy to share our experience and will probably make the code available. It's a work in progress.

Best regards, Mike Healy

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]