Dear all, The fact that the 'right' morphisms of topos theory (geometric morphisms) are not structure preserving maps gives rise to the debate below. With an entirely localic approach the situation can be recovered; but at the cost of moving from 'elementary topos' as primitive to 'category of locales'. Here geometric morphisms can be represented as adjunctions that commute with the double power locale monad and it is the double power locale monad that gives the structure in categories of locales. So there are avenues worth exploring which may provide a way of marrying up the structural disconnect between objects and morphisms that is implicit in topos theory. Christopher Subject: Re: categories: Re: Grothendieck toposes On 2016-11-01 17:16, Joyal wrote:

It is marvelous that the two notions should be so related. But it is be better to keep them appart before uniting them. Otherwise the miracle disappear in confusion.

The "miracle disappears in confusion" is an important observation, as is the need to "keep apart before uniting". Syntax and semantics is like that, or meta and object language. Foundations of mathematics without categorical consideration is basically then over Set, naively speaking. Logic is similar. Fons et origo logic from late 19th century and decades after is confused about being before set theory or after. Topos internalizes logic but is different from the Goguen-Meseguer approach to institutions and entailment systems. The apples and pears of logic should not be seen as a fruit salad. I've sometimes thought (and written some pieces about, e.g. to be found under www.glioc.com<http://www.glioc.com>) what if Gödel's Incompleteness Theorem wasn't a Theorem but a Paradox. After all, Gödel basically transforms the Liar Paradox to a Liar Theorem, and logicians at that time (except maybe Hilbert, but he was too old to quarrel) found it to be very smart. However, if we use underlying categories and functors to start from signatures, then create terms, then sentences, then entailments, then models, then proof strategies, and so on, it means we close doors behind us, so that we disable ourselves to mix truth and provability as being "of the same kind or type", which Gödel did. Categorically, terms come from monads, because they enable substitution, but sentences just from functors, because otherwise everything is 'term'. The functorial description and generality of entailment and model is of course more tricky, in particular if the underlying category is something more elaborate (like monoidal closed categories) than just Set. In this (heretic?) view, Gödel's Theorem/Paradox is actually an example where that miracle appears because of the unintended (?) confusion, so this is why I sometimes think what if it was ween as a Paradox. Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]