Peter Freyd asks
Is there a standard name for those categories, A, such that the slice category A/X is a topos for each object X in A?
Are there any theorems?
I don't know about the first question: not too sure whether I like "partial" topos - I thought of "local topos" or "polytopos". To the second, presumably Peter had some conjectures or generalisations in mind. I wonder what they were. Obviously a great many things generalise directly. For example, since experience shows that categorical logic is "local" in character - ie depending on an context (in the proof- or type-theoretic sense) - arguably the terminal ("global") object should be dropped altogether. (On the other hand, earlier discussion of generalised definitions of "regular epi" showed that others did not find my methods of translating global to "poly" definitions via slices quite as obvious as I thought they were.) Strictly with the status of an "idle musing", one application of this that occurred to me was to model theories which are globally inconsistent but locally consistent. Dov Gabbay, who is good at inventing such examples, had a nice story of a professor who sought early retirement by telling the vice-chancellor he had a weak heart but his wife that he was healthy - only when the professor's and vice-chancellor's wives met was there a contradiction. On a more serious note, I have a comment in a different direction from the discussion by Richard Wood and others on (internal) logic. The (2-)category of polytoposes, stable (wide pullback preserving) functors (and cartesian transformations) is cartesian closed, indeed it has a symmetric monoidal closed structure and a comonad inducing the CCC a la Girard. If we make the categories have and the morphisms preserve filtered colimits, and impose the additional condition that any colimit diagram in the categories which has a cocone has a colimit (equivalently that they have binary products) then we may obtain models of (stronger) forms of polymorphism, including a type of types. Reference? Sorry, not for the general case, but in the case where the slices are presheaves on groupoids, see my paper "Quantitative Domains, Groupoids and Linear Logic" in CTCS 3 (Manchester, 1989), Springer LNCS 389. Also available from theory.doc.ic.ac.uk as /theory/papers/Taylor/Quantitative.dvi but beware that the font llwith10 is needed for the par. (The irony of this is that the alleged par is not a functor.) More sketchy results to back up my claims above in the other stable domain theory papers in that directory. ======== I see "tick off", like "mad", has different meanings on the two sides of The Pond. I understand it as "criticise (lightly)". (As regards "good old Eric Partridge", I think his dictionary is (a) useless, being largely confined to the peculiar usage of individual regiments & English Public Schools, and (b) offensive - see the entry under "gay".) Finally, let me assure you that there is no slanging match between me & Make Barr (whom I should have added to the list of those with higher priorities than TeX), but it is in the nature of software that differences arise which no amount of diplomacy can (or should) resolve. Paul ==============================================================================
participants (1)
-
Paul Taylor