Date: Thu, 1 Oct 92 14:34:19 EDT From: pjf@saul.cis.upenn.edu (Peter Freyd) 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 (e.g. the category whose objects are topological spaces and whose maps are local homeomorphisms)? Are there any theorems? ============================================================================== Subj: From triposes to assemblies (correction) Date: 1 Oct 92 13:44:43 EST From: ------------- Thomas Streicher pointed out a problem in my definition of the "canonically separated" objects for triposes based on PCAs (and recall this does not simply mean the tripos given by a PCA in the most direct way). The correct definition is: The tripos construction of a topos takes as objects all pairs (X,=) where "=" is a partial equivalence relation in the sense of the tripos on the set X. To get a category of assemblies instead, take only those pairs (X,=) where = is contained (in the tripos sense) in (Exist)(delta_X)(true) In other words, those = contained in the "direct image" along the diagonal function for the set X of the maximal predicate (in the tripos sense) on X. Call these the "canonically separated" objects. In the case of the effective topos this agrees with Hyland's usage. The rest works as in the original post. These objects can be represented by assemblies and the arrows between them as ordinary set theoretic functions with moduli. That gives a regular category whose effective reflection is the topos given by the tripos. The assemblies are (up to iso) precisely the separated objects of the topos. Colin McLarty ============================================================================== Subj: diagram macros From: Paul Taylor Date: Thu, 1 Oct 1992 19:09:30 +0100 One person has ticked me off for having a shouting match with Mike Barr. I apologise. Several others have expressed sympathy, solidarity, etc. I don't think the categories list is an appropriate place for a discussion of LaTeX, so I don't want to go into any details. I just want to make an observation to settle the minds of those who are already using various packages or who are considering which one to use. Existing methods of drawing commutative diagrams may be divided, broadly speaking, into three classes: (1) use some general purpose graphics package, either within TeX (eg eepic, pictex) or by importing PostScript (eg MacDraw, CorelDraw). (2) matrix-based specialist commutative diagrams packages such as those of Francis Borceux; ftp sol.cs.ruu.nl /pub/TEX/DIAGRAM/diagram* Kris Rose (xypic); ftp ftp.diku.dk /pub/tex/misc/xypic.tar.Z Steven Smith (arrow); ftp ftp.cs.umb.edu /pub/tex/eplain/arrow.tex Mike Spivak (lamstex); june.cs.washington.edu /tex/LAMS-TeX.tar.Z me; ftp theory.doc.ic.ac.uk /tex/contrib/Taylor/tex/diagrams-V4* maybe others; please tell me if these are not the authoritative archives (3) Mike Barr's macros. If you think Mike Barr's design philosophy is the right one then (God help you) you should send your suggestions to him. If you like mice then I hope you'll be happy together. The main point is this:******************************************************* * If you use any of the five packages I've mentioned in (2) * * AND STICK TO THEIR CORE FEATURES, AVOIDING HACKS & GIMMICKS * * then you have a pretty good chance of getting continued support should the * * one you use cease to be maintained, because since their conceptual basis * * is common it will be possible to emulate or translate them. * ****************************************************************************** For example, /tex/contrib/Taylor/tex/Borceux-to-Taylor-prototype.tex is a first attempt to emulate Francis' macros using mine. Try it out if you like but don't complain if it doesn't work correctly because I know that. It's a bug-ridden prototype to demonstrate the principle. Several low-level modifications have been made to my package (or are on the agenda) to deal with the minor conceptual differences and thereby facilitate emulation. Existing users of matrix-based packages (especially those who have used more than one of them) are welcome to send me their comments on the treatment of the core features. I will collect comments and forward them to whatever committee emerges to formulate proposals for LaTeX 3. Suggestions such as Might I also mention strings, links, and Penrose tensor notation. will only cause annoyance. How many such diagrams do you envisage ever being drawn? The original question was about syntax, and you have contributed nothing to that, even if anyone were willing to implement these features. I have my own research/career to get on with, and maintain TeX primarily for that. I'm certain Francis would say the same, as probably would others. If you want special features, DIY or *pay* somebody like Spivak to do it. An experience with a certain professor (and his publisher, OUP) who got me to spend several days rewriting my macros for use in some paper about a cube, and didn't even so much as take me out for a drink afterwards, has made me dis-inclined to go very far out of my way. I'm sorry. Paul ============================================================================== Subj: Re: Freyd's question Date: Thu, 1 Oct 1992 21:59:00 +0100 From: Thomas Streicher Categories with finite limits where each slice is a topos and reindexing is the inverse image part of a geometric morphism have been called "partial topos" by J. Benabou . It are lccc-s where each slice category is a topos. He gives as example any groupoid. T. Streicher ++++++++++++++++++++++++++++++++++ Date: Fri, 2 Oct 92 12:41:15 +1000 From: street@macadam.mpce.mq.edu.au Perhaps a bicategory B which is "locally a topos" (i.e. whose hom-categories B(u,v) are topoi and for which B(f,g) is a geom morphism for all arrows f, g) might be called a *biallegory*. These provide a setting for "stacks". Of course, Peter's categories A are then those with SpanA a biallegory. Ross ++++++++++++++++++++++++++++++++++ Date: Fri, 02 Oct 92 09:46:08 +0100 From: Andrew Pitts >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 >(e.g. the category whose objects are topological spaces and whose >maps are local homeomorphisms)? Are there any theorems? You should try asking Jean Benabou about this (not, I guess, by email). I seem to remember he worked on this kind of thing a few years ago (but I can't seem to remember what the results were). Andy Pitts ============================================================================== Subj: apologies Date: Fri, 2 Oct 92 11:22:59 EDT From: pjf@saul.cis.upenn.edu (Peter Freyd) When Paul Taylor writes: "One person has ticked me off for having a shouting match with Mike Barr," what does he mean? Is this a Taylorism or a Londonism? In the American Heritage Electronic Dictionary Copyright 1991 it says: [tick off]. (Slang). To make angry or annoyed: ``got really ticked off at her refusal.'' So is Paul saying that someone made him angry for his having a shouting match? Come to think of it, it wouldn't be all that surprising. Best thoughts and always remember to be nice to mice, peter +++++++++++++++++++++++++++++++++++ Date: Fri, 2 Oct 92 12:19:20 EDT From: barr@triples.Math.McGill.CA (Michael Barr) Leaving the linguistic question aside, I would like to point out that I have never engaged in any shouting match with Paul Taylor and I don't intend to start now. Moreover, I have kept my private opinion of his posts strictly private and intend to continue that practice as well. Coming back to the linguistic question, I don't know for sure, but that is the sort of expression that can wind up with quite different usages on the two sides of the puddle, so I assume that is the case here. Michael +++++++++++++++++++++++++++++++++++ Date: Fri, 2 Oct 92 15:02:04 EDT From: barr@triples.Math.McGill.CA (Michael Barr) One of my colleagues claims that ``tick off'' is British schoolboy slang for scold. Michael ============================================================================== Subj: Octoberfest Date: Fri, 2 Oct 92 15:21:04 EDT From: barr@triples.Math.McGill.CA (Michael Barr) As it stands now, we have nine people who have asked to talk. I am happy with that number, but we could also accomodate 2 or 3 more. Here is a list of talks and, insofar as I have been provided them, with titles and abstracts. Michael Robin Cockett: TBA James R. Otto: Complexity classes from categories Richard Wood: A somewhat circular characterization of the category of sets Years ago in a paper on total categories (those locally small B for which Y=yoneda:B--->PB has a left adjoint) I observed that for B=set_ there is U-|V-|W-|X-|Y and conjectured that this characterizes set_. Bob Rosebrugh and I have returned to this recently and hope to formally announce the result very soon. It builds on our work on completely distributive lattices. It probably makes good sense to say that a category B is "totally distributive" if it admits W-|X-|Y so the result can be seen as setting bounds on how "exact" a category can be. David B. Benson: Paths in Higher-Dimensional Graphs Paths in higher-dimensional graphs have arrows between arrows. These paths abstract many aspects of programming languages and related semantical matters. Higher-dimensional graphs, a concept closely akin to computad, generate free n-categories -- and hence the free cellular omega-categories. The arrows of such categories are represented by paths as the equivalence classes of paths modulo interchange. Normal forms for the presentations of paths provide fast equality tests between the represented arrows, important for the goal of programming these ideas. Two normal forms are considered. Natural normal form arises directly from the definitions. Irreducible normal form is more efficient in the use of computer storage and appears to be related to Street's exponential wedge of r-equivalences. Thomas F. Fox: TBA Charles F. Wells: Mike Wendt: On Measurably Indexed Families of Hilbert Spaces. Robert Gordon: Tricategories Michel Hebert: A syntactic characterization of locally polypresentable categories ============================================================================== Subj: Re: diagram macros Date: Fri, 2 Oct 92 11:44:36 +1000 From: street@macadam.mpce.mq.edu.au In response to Paul Taylor's letter expressing a certain amount of annoyance, it is clearly time for a (perhaps also annoying?) parable told me by a philosophical hero of mine, Steve Schanuel. It is well known that John Isbell has an incredible ability to create counterexamples when they exist. A great load was lifted from his mind when he realized one day that he was not obliged to provide a counterexample for everyone in category theory who could not prove their conjecture! -------- But, Paul, I WILL buy a beer (maybe even a bottle of good Australian red) for anyone who does design string-drawing software I can use. In the meantime, don't worry. I'm happy with MacDraw. Best regards, _________________________________________________________ / Ross STREET \ / School of Mathematics, Physics, Computing and Electronics \ / Macquarie University, New South Wales 2109, AUSTRALIA \ / Telephone: 61-2-805-8946 Facsimile: 61-2-805-8241 \ /-----------------------------------------------------------------\ "Never cut what you can untie" Joseph Joubert ++++++++++++++++++++++++++++++++++++ From: dyetter@math.ksu.edu (David Yetter) Date: Fri, 2 Oct 92 11:18:59 CDT I have no desire to become involved in a row over design philosophy or the virtues of existing packages (I personally, despite not particularly liking mice, use xfig to draw my diagrams and export LaTeX picture code), but Paul Taylor's comment (reproduced below) on Ross Street's suggestion is ill conceived: > Suggestions such as > Might I also mention strings, links, and Penrose tensor notation. > will only cause annoyance. How many such diagrams do you envisage ever being > drawn? My most recent manusript contained fourteen figures, each with between 2 and 9 Penrose tensor diagrams. Joyal/Street's "Geometry of Tensor Calculus I" contains numerous such diagrams as do *many* recent papers on the categories of representations of quantum groups (by such people as Reshetikhin, Turaev, and Lyubasheko). A good syntax for diagrams in Penrose tensor notation, would naturally include a good syntax for drawing knot diagrams (of use to low-dimensional topologist generally) and Feynman diagrams (of use to physicists), besides being invaluable to those of us who work on applications of monoidal category theory in those areas. Obviously, LaTeX is used by many people besides categorists, and if we're going to update it to accomodate our need for algebra freed from the constraints living in linear strings of symbols, we might as well get it right for all people who need such algebra. --David Yetter ============================================================================== Subj: Regular categories From: Richard Wood Date: Fri, 2 Oct 1992 16:34:43 -0300 I was writing a very belated contribution to the earlier discussion about regular categories when I saw Peter Freyd's question about categories all of whose slices are topoi. Since the former bears on the latter here it is without further ado. The definition of Carboni and Street given in "Order ideals" is particularly nice because "E is regular" in their sense is exactly what one needs to define Rel(E) with no circumlocution. Recall that they require pullbacks, define strong epis in terms of (jointly) monic spans and require that every span factor, pullback stably, as a strong epi followed by a monic span. Then E is Barr regular iff E is C&S regular and has a terminal object. In joint (as yet unpublished) work with Carboni and Kelly we observed that the entire C&S definition can be encoded in a single adjunction. Let S be the category x<---r--->a, the "free-living" span. Let {S,E} denote the functor category, best thought of here as a power (=cotensor), and let (S,E) denote the full subcategory of it determined by the monic spans. Regard both categories and the inclusion, in:(S,E)--->{S,E} as data over ExE via the codomain(s) functors, c. Then E is a regular category iff "in" has a left adjoint "im" in the 2-category of fibrations over ExE. The point is that c:{S,E}--->ExE is a fibration iff E has pullbacks, whence c:(S,E)--->ExE is also a fibration; existence of im , merely as a functor over ExE, provides factorizations; and im being an arrow of fibrations is equivalent to stability under pullback. It is then fairly clear that one can define regular objects, E, in suitable 2-categories other than CAT, provided that one has also an interpretation for (S,E). This is not necessarily an idle generalization because such an approach dictates the reasonable definitions for both arrows and proarrows in the 2-categories of regular objects that result when regularity is studied in the presence of further properties or structure. (For a similar sort of situation consider studying (co)complete objects in the 2-category of finitely complete ordered sets where the result is locales, or the deeper idea of Kelly and Lawvere of studying finitely complete objects in the 2-category of Skolem categories.) But returning to regular categories, consider now Rel(E)(x,a) (where x and a are objects of E). It is reasonable to ask for representability in a , by an object P_a (but better S_a for see below). This was proposed by Street in the 1972 "Christmas card". C&S regular categories with this property, let us call one such an "opos" are rather good. In fact, E is a topos iff E is an opos and has a terminal object. (I believe that such categories have been considered by Benabou in work on trees and by Taylor in connection with laminations.) Every slice of an opos is a topos and if E is an opos then all Spn(E)(x,a) are again oposes. The present definition indicates that in addition to topoi, groupoids (and hence sets) are oposes. Another interesting example suggested by Pare is the category whose objects are topological spaces and whose arrows are local homeomorphisms. Still another is the category whose objects are sets and whose arrows are functions with finite fibres. The last example indicates that Cantor's theorem can fail in a non-degenerate opos, for there P_a is the set of finite subsets of a. It is probably better to write S_a for P_a and think along the lines of Joyal and Moerdijk as in their "Cumulative hierarchy of sets" paper. Although the diagonal argument has many forms, as Lawvere showed, one sees here that it is in a certain sense inevitable. On the geometric side one gains intuition about oposes by observing that a disjoint union of oposes is again an opos. The geometric intuition is further sharpened by recalling that functors between topoi that have pullback preserving left adjoints can be thought of as both partially defined geometric morphisms and families of geometric morphisms. These have been studied by Kennison, Pare, Thiebaud, Rosebrugh and the writer. The chief virtue of oposes seems to be that 2-categories of such are easier to work in than TOP, the 2-category of topoi and geometric morphisms.The 2-categories of oposes that I refer to are oposes together with fuctors that have pullback and monic span preserving left adjoints and natural transformations; oposes together with pullback and monic span preserving functors and natural transformations in the opposite direction. (The reason for dualizing at the level of 2-cells is so that the inclusion of the former in the latter is proarrow equipment as discussed in various papers by Rosebrugh and the writer. It enables a direct analogy with the pardigm CAT--->PRO, where the 1-arrows of PRO are profunctors.) It appears that various inverse limit constructions in TOP and related 2-categories have their complications concentrated in the passage from oposes to topoi but I have not yet thought this through. By the way, part of the reason that the "pro" version of a 2-category of oposes is so simple just resides in the trivial observation that naming an object, i, of an opos E by the functor i:1--->E is pullback preserving. While I am not entirely happy with the name "opos" and do not wish to tamper with the definition of topos there are several other indications that the role of the terminal object needs to be carefully understood. One concerns the real closed unit interval [0,1] regarded as a CCD lattice. The defining left adjoint to the supremum function for down-closed subsets preserves binary infima but not the top element. This suggests that [0,1), equivalently the non-negative reals, be studied in the spirit of the CCD programme but with arbitrary suprema replaced by suprema of bounded (down-closed) subsets. Another concerns the fact that the functor U:set--->CAT(set^op,set) is pullback preserving, where U-|V-|W-|X-|Yoneda . Rosebrugh and I have recently shown that if a locally small category B has such an adjoint string as above then B is equivalent to the category of sets. Regards, R.J. Wood ============================================================================== Subj: Re: apologies Date: Sat, 3 Oct 92 12:15:40 EDT From: pjf@saul.cis.upenn.edu (Peter Freyd) The OED records only the American use of "ticked off" and dates it to 1959. But good old Eric Partridge says that by 1916 it meant (in the British military): "to reproach, upbraid, blame; esp. to reprimand." (A Dictionary of Slang and Unconventional English, 8th Edition, 1984.) ============================================================================== Subj: Re: Regular categories From: koslowj@math.ksu.edu (Juergen Koslowski) Date: Sat, 3 Oct 92 11:07:38 CDT This concerns Richard Wood's remarks on regular categories: Maybe this is a superficial observation, but the terminal object in a topos and the 1 in a ccd lattice are the unit elements with respect to cartesian product x and binary meet, respectively. I seem to remember that such unit objects are responsible for difficulties when proving nice coherence theorems (maybe Richard Blute could comment on that). Also, from computer scientists I got the impression that a unit object with respect to pairing causes complications in the lambda calculus. In particular the isomorphism A \cong [I,A] causes lots of trouble with the "continuation passing style transformation" some computer scientists like to use. I wonder whether it is this aspect of the terminal objects that is responsible for the complications Richard Wood describes. -- J"urgen -- J"urgen Koslowski | If I don't see you no more in this world Department of Mathematics | I meet you in the next world Kansas State University | and don't be late! koslowj@math.ksu.edu | Jimi Hendrix (Voodoo Chile) ============================================================================== Subj: Note from moderator Date: Sat, 3 Oct 1992 17:22:24 -0300 (ADT) From: Bob Rosebrugh Based on the the desire to allow discussion to flow freely, I have recently posted several messages which do not obviously qualify as discussion of category theory. Without criticizing either the posters or myself (for letting these posts go out), I will query (but not censor) future posts which are not clearly related to category theory. It should be noted that general discussion of aspects of (La)TeX or other programs which are widely useful in the community are clearly related to category theory. Regards to all, Bob Rosebrugh ============================================================================== Subj: Re: apologies Date: Mon, 05 Oct 92 10:19:45 From: sjv@doc.ic.ac.uk (Steve Vickers) [Sorry to prolong a non-categorical thread - I hope I'm not saying anything contentious enough to warrant a reply.] I can state without recourse to dictionaries that in living English English, to tick off is to reprimand, e.g. "Teacher gave me a real ticking off." Paul's usage ("One person has ticked me off for ...") was completely idiomatic. I only found out this year that American English is different - the phrase is used in the "annoy" sense on "Dinosaurs". Steve Vickers ============================================================================== Subj: categories whose slices are toposes From: Paul Taylor Date: Mon, 5 Oct 1992 12:46:29 +0100 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 ============================================================================== Subj: diagrams yet again From: Paul Taylor Date: Mon, 5 Oct 1992 16:08:17 +0100 Having criticised (ticked off) certain senior categorists for giving terse and uninformative answers to naive category theory questions, perhaps I ought to give more helpful responses to TeX questions. LaTeX 3 is a general and extensive re-write of LaTeX. I don't fully understand the terms of reference, though they started as making amstex work with LaTeX. Some very amateurish CDs were in amstex, so we may take it that the present objectives are to do (ie make compatible and recommend a package to do) that much, but more professionally. There were CDs in amstex because (presumably) whoever at AMS specified it considered that they were already an important mode of expression IN MATHEMATICS AS A WHOLE. Rectangular diagrams without 2-cells are very commonly found. We all know exactly what the idiomatic usage of such diagrams is and that we would be lost without them. Moreover the fact that Mike Spivak, Steven Smith, Kris Rose and I have put a lot of time into developing the matrix notation of TeXercise 18.46, that Francis Borceux came up with the same idiom without reading the TeXbook, and that large numbers of users have found these five packages convenient are evidence that this is the most appropriate way of rendering such diagrams in machine- (and, of course, user-) readable form. The strings, braids, etc., are a completely different matter. It is not belittling the work done on these topics, in Australia in particular, to say that they are of minority interest, compared to the use of the simpler forms of diagrams. Nor would I be accusing Ross of riding a bandwagon if I suggest that in five years' time he'll probably be interested in something else and drawing a completely different kind of diagram. Meanwhile others on the fringe of the expanding categorical cosmos will only just be learning to use commutative \square's. With such a major piece of programming as CD drawing, "what you see" (type) and "what you get" (see on paper) are completely different things and are to be thought of (designed) separately. For example, the diagrams in my thesis (as submitted to Cambridge in 1986) look pretty horrible, but substituting a recent version of my diagrams package (and, I confess, a little bit of global editting) yields an aesthetically far superior result for (almost) the same input. Later (say post Sept 1989) sources are adapted more easily. I have continued to support the same input language whilst developing the output. With the exception of a few details, the original language design decisions turned out to be good ones. Those who have asked me in person "how do you do this in TeX" will have found that I have tricks up my sleeve which I use in my own papers but am reluctant to explain. Other things have had loud "PROTOTYPE" warning messages in them. This is because any piece of code I give out I have a duty to maintain (in the sense I've mentioned, of continuing to parse the input and producing similar or better output), so until I'm sure that I'm happy with the input language I won't release things. Consequently I sometimes get overtaken. So the short answer to Ross's comment (at the risk of compromising my own typographical principles and contradicting Mike Barr's recent [private] comment to me, "Hell, at least we agree on TeX!" :-) ), is, you're right in sticking to MacDraw for what are for the time being ad hoc diagrams. You can use epsf.sty to import them into LaTeX documents. That is after all the modern equivalent of getting the engraver to do it. When the idiom has become clear, and you've got me sufficiently interested in the subject to want to draw the diagrams myself, then I'll write your macros. Paul ============================================================================== Subj: Ross' request Date: Mon, 5 Oct 92 16:53:14 EDT From: barr@triples.Math.McGill.CA (Michael Barr) I consider Ross' request perfectly reasonable. I actually have done some of these for Marta. More to the point, I don't think that anyone ought, in principle, decide that any particular notation is not important enough to do, just because some especial package doesn't do it. I don't even exclude the upside-down ampersand, although I don't care for it at all. As I just got finished saying on another forum, we ought to be trying to include people, not exclude them. By the way, I considered the pitiful attempt to do commutative diagrams in AMS-TeX as AMS' expression of their contempt for category theory, rather than as any genunine attempt to accommodate us. Michael ============================================================================== Subj: Re: diagrams yet again Date: 05 Oct 92 20:07:34 PDT (Mon) From: pratt@cs.stanford.edu From: Paul Taylor Date: Mon, 5 Oct 1992 16:08:17 +0100 The strings, braids, etc., are a completely different matter. It is not belittling the work done on these topics, in Australia in particular, to say that they are of minority interest, compared to the use of the simpler forms of diagrams. Paul's representation of strings and braids as a flash in the category theory pan is not borne out by the literature. Strings have been an integral part of the arrow business for a long time, witness Psalms 21:12, "Therefore shalt thou make them turn their back, when thou shalt make ready thine arrows upon thy strings against the face of them." Besides their supporting role with arrows, strings are also known to every linguist and computer scientist to be an integral part of language, as Mark 7:35 attests: "And straightway his ears were opened, and the string of his tongue was loosed, and he spake plain." Commutative algebra has been synonymous with mainstream algebra for a long time. But noncommutative algebra has been more than just a cottage industry for many years, and moreover has found a warmer welcome in linguistics and CS than the commutative variety, providing us with an algebraic basis for Turing machine computations and formal grammar derivations, both of which can be conveniently laid out in the (oriented) plane, where they lend themselves to a 2-categorical formulation. But as Zadeh reminds us, we live in a fuzzy world, neither clearly commutative nor clearly orientedly planar, but somewhere in between. The laws of this in-between world are braidal, with planarity corresponding to the initial or discrete braids and commutativity to the final braids, which can pass through themselves without losing their identity altogether (commutativity without idempotence). Under these circumstances we can only keep our 2-categorical cool with braids, suggesting the following slogan: Braids are the rule, of which commutativity and noncommutativity are its two extremes. This appears to be a natural idea in both senses of "natural." It is a natural mathematical idea to suggest and pursue; and it appears to be one that can be found in nature, witness the Yang-Baxter equations arising early on in physics, whose braidal character is now clear and about which several mathematical physicists have started writing, e.g. John Baez's recent MIT lecture notes on "Braids and Quantization." Nor would I be accusing Ross of riding a bandwagon if I suggest that in five years' time he'll probably be interested in something else and drawing a completely different kind of diagram. Nor would I be calling Paul shortsighted if I suggest that in five years time many of us in both mathematics and physics, and conceivably even philosophy, will be drawing braids. (This is not to suggest that Jon Barwise's reaction to my explanation of linear logic last February would have been any different had I omitted the section on braids, which included five braid diagrams I had to do in ASCII that I am looking forward to being able to render in Taylorese.) As for Ross, I rather expect that in five years time he will be drawing whatever it is that those of us in the trenches will be drawing in ten years time, and one might hope that these too would appear in some diagram package, preferably in 1997 rather than 2002. Meanwhile others on the fringe of the expanding categorical cosmos will only just be learning to use commutative \square's. This brings me back to my first theme. Categories have been a pons asinorum for "the rest of us" for a very long time, ever since the exam in category theory given to the young lad who appeared briefly in the story of David and Jonathan [I Samuel 20:21-22]: And, behold, I will send a lad, saying, "Go, find out the arrows." If I expressly say unto the lad, "Behold, the arrows are on this side of thee, take them;" then come thou: for there is peace to thee, and no hurt; as the Lord liveth. But if I say thus unto the young man, "Behold, the arrows are beyond thee;" go thy way: for the LORD hath sent thee away. As it turned out the arrows were indeed beyond the lad, who "knew not anything, only David and Jonathan knew the matter," and the lad was sent off to the city [20:37-40], a drop-out who for all we know may have later become the Bill Gates of his day. Another biblical character who struggled mightily with the subject was Job. "For the arrows of the Almighty are within me, the poison whereof drinketh up my spirit: the terrors of God do set themselves in array against me." [Job 6:4] One imagines him tackling either metacategories or coherence on that occasion. Job was thus afflicted for a long time, during which he complained bitterly of his plight to his three friends and the Lord in three major jam-sessions. In the last of these, the Lord showed up in a Whirlwind evidently hoping to be able undo Satan's mischief and set things straight at last. After spending the better part of three chapters extolling the virtues of His nobler creatures and getting Job into the proper frame of mind, the Lord came to the whale, of which He said "The arrow cannot make him flee." [Job 41:28] That apparently did the trick: Job immediately apologized for his ignorance of the subject: "I have heard of thee by the hearing of the ear, but now mine eye seeth thee. Wherefore I abhor myself, and repent in dust and ashes." [Job 42:5-6]. The Lord then in unexpectedly firm tones told Job's friends that Job now understood the subject better even than they did and to treat him properly henceforth. And He gave Job twice what he had before. This came to 14,000 sheep, 6,000 camels, 1,000 oxen, 1,000 she-asses, 7 sons, and 3 daughters, so you can figure out what he had before, at least for the livestock. If Job's arrow anxiety lasted 25-35 years, that's around 2-3% p.a., probably a good rate for those days. But I digress. Anyway you can read it for yourself, you'll see it's exactly as I said. Coming from the electrical engineering side of the business myself, the advice to "Cast forth lightning, and scatter them: shoot out thine arrows, and destroy them." [Psalms 144:6] speaks more directly to me. Vaughan Pratt ============================================================================== Subj: Ross' request Date: Tue, 6 Oct 92 08:09:18 GMT-0400 From: jds@rademacher.math.upenn.edu Begin forwarded message: Date: Mon, 5 Oct 92 16:53:14 EDT From: barr@triples.Math.McGill.CA (Michael Barr) I By the way, I considered the pitiful attempt to do commutative diagrams in AMS-TeX as AMS' expression of their contempt for category theory, rather than as any genunine attempt to accommodate us. Michael End forwarded msg: I don't want to tick anyone off nor for them to be ticked off, but that is a rather parochial comment. There are (a few!) other users of commutative diagrams! jim stasheff ============================================================================== Subj: Re: diagrams yet again Date: Tue, 6 Oct 1992 19:59:40 +0100 Thanks to Vaughan for putting a literary slant on this which I can't match. Please excuse me if *I* adopt a conservative policy and only provide macros which I believe I can support, with orthogonal design, in the long term. If Mike Barr or Kris Rose or anyone else wants to fill the niche markets with their non-orthogonal methods, that's fine by me. Just remember the "general advice" I gave earlier. Paul ============================================================================== Subj: Re: diagrams yet again Date: 6 Oct 92 11:51:07 EDT From: Charles Wells > Besides their supporting role with arrows, strings are also known to > every linguist and computer scientist to be an integral part of > language, as Mark 7:35 attests: "And straightway his ears were opened, > and the string of his tongue was loosed, and he spake plain." (Apparently Vaughn just acquired the King James Version on CD ROM.) The Hebrews and Greeks wrote in strings, as we do, but the Egyptians and Chinese wrote in pictures. Freyd has worked out the beginnings of a diagram-based language, although his statements still appear as strings of diagrams. (Egyptian cartouches, I would argue, are truly not strings.) Atish Bagchi and I will show how logic can be based directly on graphs and diagrams (not strings of them) in our forthcoming paper, "Graph- based logic and sketches." In this case, "forthcoming" probably means in a few months. I will talk about it in Montreal this weekend. (This is a commercial.) Several times lately Vaughn has posted interesting messages on one forum or another and I have answered by criticizing minuscule parts of what he says. Illegitimi non carborundum, Vaughn. One theme in his messages (as I perceive it) is that category theory appears unnecessarily arcane to the rest of the technical world. Let us take heed. -- Charles Wells Department of Mathematics, Case Western Reserve University University Circle, Cleveland, OH 44106-7058, USA 216 368 2893 ============================================================================== Subj: VAUGHAN Pratt Date: 7 Oct 92 14:28:18 EDT From: Charles Wells I repeatedly misspelled his name in my last message. Sorry. -- Charles Wells Department of Mathematics, Case Western Reserve University University Circle, Cleveland, OH 44106-7058, USA 216 368 2893 ============================================================================== Subj: update to speaker's list Date: Wed, 7 Oct 92 18:44:21 EDT From: barr@triples.Math.McGill.CA (Michael Barr) Titles and some abstracts - Michael Barr: Cohomology of algebras Consider an adjunction F -| U, U: *A* --> *B* and F: *B* --> *A*. Suppose that *A* is a regular category and U a regular functor. Let T and G be the resultant triple and cotriple. Assume that B projective in *B* implies that TB is projective. Suppose the inclusion Ab(*A*) --> *A* has a left adjoint Diff. Suppose there is a chain complex functor C.: *A* --> ChComp(Ab(*A*)) that produces, for each A of *A*, for which UA is projective, a projective resolution of Diff(A). Suppose also that for each n >= 0, there is a ~C_n: *B* --> Ab(*A*) such that ~C_n o U = C_n (= here means natural equivalence). Then for any A of *A* such that UA is projective and any M of Ab(*A*), we have H^._G(A,M)=Ext^.(Diff(A),M). Applications include the well-known equivalence of the Hochschild cohomology of associative algebras with the cotriple cohomology for algebras that are projective over the ground ring, as well as that of the Eilenberg-Mac Lane cohomology of groups with the cotriple cohomology, but also gives the analogous result for Lie algebras, which has not, to my knowledge, been previously published. - David B. Benson: Paths in Higher-Dimensional Graphs Paths in higher-dimensional graphs have arrows between arrows. These paths abstract many aspects of programming languages and related semantical matters. Higher-dimensional graphs, a concept closely akin to computad, generate free n-categories -- and hence the free cellular omega-categories. The arrows of such categories are represented by paths as the equivalence classes of paths modulo interchange. Normal forms for the presentations of paths provide fast equality tests between the represented arrows, important for the goal of programming these ideas. Two normal forms are considered. Natural normal form arises directly from the definitions. Irreducible normal form is more efficient in the use of computer storage and appears to be related to Street's exponential wedge of r-equivalences. - Richard Blute: Proof Nets and Monoidal Categories - William Boshuck: Strong completeness of predicate modal logic or A duality theorem for predicate modal logic - Robin Cockett: TBA - Peter J. Freyd: Path Integrals - Robert Gordon: Tricategories - Michael Hebert: Syntactic characterizations of closure under pullbacks and of locally polypresentable categories Locally (finitely) polypresentable, resp. multipresentable, resp. presentable categories (LFPP, LFMP, LFP) are (finitely) accessible categories with wide pullbacks, resp. connected limits, resp. all (small) limits. LFPP are also fin. acc. cat. having all its slices LFP (Example: the algebraically closed fields). LFMP have been syntactically described by Johnstone in 1979, LFP by Coste in 1976. My first result is a syntactic description of LFPP in this spirit. If we now start with a given (finitary) language and want to stay within, and require the limits to be the "usual" ones, they correspond to elementary categories of models closed respectively under pullbacks (LFPP), equalizers and pullbacks (LFMP) and finite limits (LFP). Syntactic characterizations become somewhat more complicated; LFP case was solved by H.Volger in 1979 and LFMP case by myself in 1991. I will present the solution for the pullback case. Those two results solve problems respectively presented by F. Lamarche (in the context of Domain Theory) and by H.Volger (in the context of classical Model Theory, with motivations also from Database Theory). - Hongde Hu: A duality theorem on accessible exact categories - James R. Otto: Complexity classes from categories - Richard Squire: TBA - Walter Tholen: Factorization Systems as Eilenberg-Moore Algebras - Charles F. Wells: Graph Based Logic and Sketches - Mike Wendt: On Measurably Indexed Families of Hilbert Spaces. - Richard Wood: A somewhat circular characterization of the category of sets Years ago in a paper on total categories (those locally small B for which Y=yoneda:B--->PB has a left adjoint) I observed that for B=set_ there is U-|V-|W-|X-|Y and conjectured that this characterizes set_. Bob Rosebrugh and I have returned to this recently and hope to formally announce the result very soon. It builds on our work on completely distributive lattices. It probably makes good sense to say that a category B is "totally distributive" if it admits W-|X-|Y so the result can be seen as setting bounds on how "exact" a category can be. - Marek Zawadowski: Lax Descent Theorems for Left Exact Categories ============================================================================== Date: Thu, 8 Oct 92 11:55:59 +1000 From: domv@macadam.mpce.mq.edu.au . . . Secondly to announce that yesterday (Wednesday the 8th October) Mike and Fiona Johnson took delivery of a brand new baby boy. Mother and child are both doing very well. I suppose I should leave it up to Mike to supply any further information, but I would like to extend my warmest congratulations to all three of them. Dominic Verity, Macquarie University, NSW, Australia ============================================================================== Subj: Re: diagrams yet again Date: Thu, 8 Oct 1992 12:06:37 +0000 From: jrk@information-systems.east-anglia.ac.uk (Richard Kennaway) This message has nothing to do with categories, but that's the point. Paul Taylor writes: >LaTeX 3 is a general and extensive re-write of LaTeX. I don't fully understand >the terms of reference, though they started as making amstex work with LaTeX. >Some very amateurish CDs were in amstex, so we may take it that the present >objectives are to do (ie make compatible and recommend a package to do) >that much, but more professionally. There were CDs in amstex because >(presumably) whoever at AMS specified it considered that they were already >an important mode of expression IN MATHEMATICS AS A WHOLE. Why the emphasis on category diagrams? Obviously, we want to be able to do them easily in LaTeX, because it's a topic we're interested in, but I would rather that LaTeX was extended with an entire language for drawing pictures, instead of just a few special cases like category diagrams, braids, inverted ampersands, and so on. (I don't consider embedded postscript to be practical for this purpose.) Has anything like this been considered by whoever is designing LaTeX 3, or by anyone else? -- Richard Kennaway SYS, University of East Anglia, Norwich NR4 7TJ, U.K. Internet: jrk@sys.uea.ac.uk uucp: ...mcsun!ukc!uea-sys!jrk ============================================================================== Subj: Graph Based Logic and Sketches Date: Fri, 9 Oct 92 12:04:58 -0400 From: cfw2@po.CWRU.Edu (Charles F. Wells) Graph-based Logic and Sketches Atish Bagchi and Charles Wells October 9, 1992 Extended Abstract Traditional treatments of formal logic provide: 1. A syntax for formulas. The formulas are typically defined recursively by a production system (grammar). 2. An inference relation between sets of formulas. This may be given by structural induction on the syntax for the formulas. 3. A rule for assigning meaning to formulas (semantics) that is sound with respect to the inference relation. The semantics may also be given by structural induction on the syntax of the formulas. First order logic, the logic and semantics of programming languages, and the languages that have been formulated for various kinds of categories are all commonly described in this way. The formulas in those logics are strings of symbols that are ultimately modeled on the sentences mathematicians speak and write when proving theorems. Mathematicians with a categorial orientation frequently state and prove theorems using graphs and diagrams (which may be described as graphs labeled coherently by data from some category). The graph, diagrams, cones and other data of a sketch are formal objects that correspond to the graphs and diagrams used by such mathematicians in much the same way as the formulas of traditional logic correspond to the sentences mathematicians use in proofs. The functorial semantics of sketches is sound in the informal sense that it preserves (usually by definition!) the structures given in the sketch. The analogy to traditional model theory is close enough that sketches and their models fit the definition of "institution" (Goguen and Burstall [2]), which is an abstraction of model theory. The content of this paper is to exhibit the structure in sketch theory that corresponds to items 1 and 2 in the description of logic (the deductive structure) and to provide a detailed translation of a particular logic between the string-based version and the sketch-based version. This work is parametrized by the type of categorial theory being considered. We assume given a finite-limit (projective) sketch E of a particular type of category as in [5] or [7]. E presents the type of category as essentially algebraic over the theory of categories. E -categories are then the models of E in Set. The kinds of categories that can be described in this way include categories with finite products, categories with limits or colimits over any particular set of diagrams, cartesian closed categories, regular categories, toposes, and many others. A formula in this setting is a potential factorization (PF) through a subobject of the codomain: formally, a pair consisting of an arrow of E and a subobject of the codomain of the arrow. We will refer to the codomain of the arrow as the codomain of the PF, and the subobject as the "claim" of the PF. Roughly, the PF is "true" if its arrow factors through its claim. Sentences are PF's whose arrows have domain 1. We provide a general recursive construction of the objects and arrows of E (hence of the PF's in particular) which is derived from the similar recursive construction for initial algebras of FLS sketches given by Barr and the second author in [8]. Our thesis is that this recursive definition constitutes the rules of inference corresponding to item 2 above. An E-sketch is a sketch that allows the specification of any kind of construction that can be made in an E-category. This greatly enhances the expressive power of sketches when compared to Ehresmann's original definition. An E-sketch is a global element adjoined freely to E ([5] and [7]). The codomain of this adjoined arrow may be perceived as a description of the graph, diagrams and other constructions of the sketch. Adjoining such an arrow constitutes the axioms of a theory, and the factorization of arrows through subobjects in the polynomial category E[s] obtained by adjoining such an arrow constitute the formulas and sentences that can be inferred from the sketch. The resulting system of inference is sound with respect to models. This type of logic fits some of the abstractions of logic that have been given, such as that of Meseguer in [4] and the formulation in terms of closures given by Tarski [6]. As a kind of worked example, the paper will also contain a detailed description of the relationship between finite-product sketches and multisorted equational logic as given by Goguen and Meseguer [3]. It is intended that this translation be sufficiently algorithmic as to be implementable, for example in Mathematica. The equations of equational logic will be seen to correspond to a specific subset of the set of PF's; indeed, in the classifying topos of E, there is a specific object and subobject that is the common codomain and claim of the all the PF's. We will give explicit proofs of the correctness of the rules of inference given by Goguen and Meseguer in terms of the deductive system described above (the recursive construction of E). References [1]M. Barr and C. Wells, Category theory for computing science. Prentice-Hall International (1990). [2]J. A. Goguen and R. M. Burstall, A study in the foundations of programming methodology: specifications, institutions, charters and parchments. In D. Pitt et al., eds., Category Theory and Computer Programming. Lecture Notes in Computer Science 240, Springer-Verlag (1986), 313-333. [3]J. A. Goguen and J. Meseguer, Completeness of many-sorted equational logic. Technical Report CSL-135, SRI International Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA (1982). [4]J. Meseguer, General Logics. Report SRI-CSL-89-5, SRI International, Computer Science Laboratory, 333 Ravenswood Ave., Menlo Park, CA 94025, USA (1989). [5]A. J. Power and C. Wells, A formalism for the specification of essentially-algebraic structures in 2-categories. Mathematical Structures in Computer Science 2 (1992), 1-28. [6]A. Tarski, On some fundamental concepts of metamathematics. In Logic, Semantics, Metamathematics, Oxford University Press, 1956. [7]C. Wells, A generalization of the concept of sketch. Theoretical Computer Science 70 (1990), 159-178. [8]C. Wells and Michael Barr, The formal description of data types using sketches. In M. Main, A. MElton, M. Mislove and D. Schmidt, editors, Mathematical Foundations of Programming Language Semantics, Springer Lecture Notes in Computer Science 298. Springer-Verlag, 1988. Atish Bagchi Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA axb35@po.cwru.edu Charles Wells Department of Mathematics Case Western Reserve University University Circle Cleveland, OH 44106-7058, USA cfw2@po.cwru.edu  ============================================================================== Subj: Re: diagrams yet again Date: 08 Oct 92 18:32:41 PDT (Thu) From: pratt@cs.stanford.edu One theme in his messages (as I perceive it) is that category theory appears unnecessarily arcane to the rest of the technical world. Let us take heed. I understand that in response to public pressure Mattel will be changing Barbie's complaint to "Category theory is tough," with the expectation that any remaining protests will be unintelligible to the media. -Vaughan ============================================================================== Subj: Complete Distributivity paper - abstract/ftp Date: October 13, 1992 From: rrosebrugh@mta.ca (Bob Rosebrugh) The preprint whose abstract follows is available by anonymous ftp from the machine sun1.mta.ca in the directory pub/papers/rosebrugh as ccd4.{tex,dvi}. The source file is LaTeX and also requires the files catmac.sty (for diagram macros) and cat.bib which are found in the same directory. Paper copies are available from Rosebrugh - be sure to include a postal address if requesting one. Constructive complete distributivity IV Robert Rosebrugh and R. J. Wood Abstract A complete lattice L is constructively completely distributive, ccd, when the sup arrow from down-closed subobjects of L to L has a left adjoint. The Karoubian envelope of the (bi-)category of relations is equivalent to the (bi-)category of ccd lattices and sup-preserving arrows. The equivalence restricts to an equivalence between ideals and ``totally algebraic'' lattices. Both equivalences have left exact versions. As applications we characterize projective sup lattices and recover a known characterization of projective frames. Also, the known characterization of nuclear sup lattices in set as completely distributive lattices is extended to an equivalence with ccd lattices in a topos. ============================================================================== Subj: weak toposes Date: 13 Oct 92 12:54:00 EST From: ------------- Does anyone have any advice about this following proposed terminology? I think I want to use the term "weak topos" to mean a cartesian closed category with all finite limits and colimits, stable surjections, and a weak power object. By a "weak power object" I mean an object W with a monic M>--->W such that every monic in the category is a pullback of M in at least one way. The reasons for this are that categories of assemblies (including assemblies for extensional or modified realizability) have these properties and: 1) Except for the part about colimits this is just what you need to show the effective reflection is a topos. 2) Using the presence of coequalizers this gives a usable generalization of geometric morphisms. If a functor between weak toposes in this sense has a left exact left adjoint then that adjoint is regular (pres. finite limits and surjections) and the adjunction lifts to a geometric morphism between the toposes. And in fact these arise among categories of assemblies (as is in effect remarked by Pitts and more recently Oosten). Thanks, Colin ============================================================================== Subj: Re: weak toposes Date: Wed, 14 Oct 92 09:19:06 EDT From: pjf@saul.cis.upenn.edu (Peter Freyd) In the early 60's Eilenberg, Mac Lane and I had lunch in a Denver cafeteria to see if we could agree on various items of terminology. There was one thing we all agreed on: the prefex "weak-" was an operator on definitions that removed uniqueness conditions. Colin's candidate for "weak topos" is only missing one of the uniqueness conditions, so I would hesitate to use the term. How about "near topos"? Best thoughts, peter ============================================================================== Subj: Re: weak toposes From: Paul Taylor Date: Wed, 14 Oct 1992 18:17:57 +0100 Peter Freyd says, > Colin's candidate for "weak topos" is only missing one of the uniqueness > conditions, so I would hesitate to use the term. How about "near topos"? Two counterarguments to this (without intending to express a definitive view): (1) There's always a danger of proliferating prefixes for "inferior" forms of things - pseudo, quasi, pre, weak, near, etc. Are you, Peter, willing to propose a definitive meaning for "near" analogous to your (& Sammy & Sauders') meaning for "weak"? Do you think we should use up one of these words for this purpose? (2) You say that a weak topos should be something satisfying the definition of a topos with uniqueness deleted *everywhere*. The first clause of this definition is that it's a category; do you intend it to be a weak category? What is that? Something (like homotopies, perhaps) which has non-unique composition? I suspect this leads us to a structure bearing little relationship to simple type theory or higher order predicate calculus. We often think of categorical definitions such as toposes in a hierarchical way, eg "A TOPOS is a cartesian category in which each object has a powerobject" (Categories, Allegories, 1.9). Here "cartesian category" is a background definition (genus in philosphical jargon) and "... powerobject" is the distinguishing property we have in mind (species) (cf bounded comprehension) So, if we want to weaken the definition, we do so by weakening the distinguishing property. n'est ce pas? Maybe this is a question that should be answered by examining what interesting phenomena arise in the literature. Raymond Hoofman's thesis ("Non-stable Models of Linear Logic", R.U. Utrecht, 1992) might be a good place to start. He considers weak cartesian closed categories - useful for modelling beta without eta in the lambda calculus. Exactly what to weaken is not, a priori, a clear cut issue. Paul ============================================================================== Subj: Re: weak toposes From: piggy@hilbert.maths.utas.edu.au (La Monte Yarroll) Date: Thu, 15 Oct 92 12:55:33 EST > > Paul Taylor writes, > > Peter Freyd says, > > Colin's candidate for "weak topos" is only missing one of the uniqueness > > conditions, so I would hesitate to use the term. How about "near topos"? ... > Are you, Peter, willing to propose a definitive meaning for "near" > analogous to your (& Sammy & Sauders') meaning for "weak"? ... > Exactly what to weaken is not, a priori, a clear cut issue. The prefix word "weak" is defined to mean "missing uniqueness", so it seems appropriate for Colin's work (or am I mistaken here?). The problem seems to be that there are degrees of "weak" imaginable. Why not provide an outside tag to identify the terminology? Colin should use "weak topos" throughout his own work; works by third persons should refer to "weak topos (as per McLarty)". ============================================================================== Subj: Re: weak toposes Date: Thu, 15 Oct 92 19:43:10 EDT From: pjf@saul.cis.upenn.edu (Peter Freyd) Paul Taylor has given good evidence on why one should avoid using the prefix "weak" when it leads to ambiguities. He says: "A TOPOS is a cartesian category in which each object has a powerobject" (Categories, Allegories, 1.9). Here "cartesian category" is a background definition (genus in philosphical jargon) and "... powerobject" is the distinguishing property we have in mind (species) (cf bounded comprehension) So, if we want to weaken the definition, we do so by weakening the distinguishing property. This gives a different notion of weak topos than McLarty's. In particular, it would have only weak exponentials whereas McLarty's has plain exponentials and a weak subobject-classifier (hence weak powerobjects). La Monte Yarroll says: Why not provide an outside tag to identify the terminology? Colin should use "weak topos" throughout his own work; works by third persons should refer to "weak topos (as per McLarty)". The trouble is, of course, the last phrase will inevitably be changed to "McLarty-weak topos". ============================================================================== Subj: position announcement Date: Thu, 15 Oct 92 12:30:53 -0700 From: dbenson@yoda.eecs.wsu.edu (David B. Benson) Dear Colleague, These positions do not appear to be well-publicized and I solicit your cooperation in making these positions more widely known. Please feel free to distribute this position announcment to all who might be interested or might be willing to cooperate in further redistributing this announcement. I believe we have 4 to 6 vacancies we can fill if a good match can be made. We are very interested in making some appointments at the the rank of associate professor and professor. Thank you for your kind assistance, David B. Benson P.S. The chair of the search committee this year is Prof. Raghu Raghavendra, raghu@eecs.wsu.edu ----------------------------------------------------------------- Computer Science Faculty Positions School of Electrical Engineering and Computer Science Washington State University The School of Electrical Engineering and Computer Science solicits applications for one or more permanent computer science faculty positions. Responsibilities include initiation and supervision of research programs and instruction at undergraduate and graduate levels. Applicants for assistant professorships should demonstrate the potential for excellence in research. Applicants for associate and full professorships should have proven records of accomplishment in their fields as evidenced by sponsored research programs and publications. We seek outstanding candidates from all areas of computer science. Areas of particular interest include software engineering, artificial intelligence, parallel and distributed computing, database theory, and theoretical computer science. Screening of applications will begin immediately and continue until the positions are filled. Positions start on January 15 and August 15, 1993. Washington State University has offered the Ph.D. in computer science since 1970, and also offers B.S. and M.S. degrees. The School of EECS has over forty faculty (approximately fifteen with primary interests in computer science and engineering), sixty computer science graduate students, and active research groups devoted to parallel and distributed processing, imaging (computer graphics, visualization, image processing, and vision), neural networks, and other areas. Computing facilities in the School of EECS include PCs, graphics workstations, and servers, all with Internet access. WSU has about 16,000 students and is located in Pullman, a quiet university town in the southeast corner of the state (approximately 90 miles south of Spokane). Nearby are some of the nation's most pristine and uncrowded places for outdoor recreation. The Pullman school system is widely acknowledged to be one of the very finest in the Pacific Northwest. Applicants should send a cover letter, a curriculum vita, and the names and addresses of three references qualified to comment on their research and teaching qualifications to Chair, Computer Science Search Committee School of Electrical Engineering and Computer Science Washington State University Pullman, WA 99164-2752 WSU is an EO/AA educator and employer. Protected group members are encouraged to apply. ============================================================================== Subj: The theorem I didn't talk about at the Octoberfest Date: Tue, 20 Oct 92 11:12:19 EDT From: barr@triples.Math.McGill.CA (Michael Barr) Consider the following situation. An adjoint pair U --| F, U:*A* --> *X*. I assume that *A* is a regular category and U a regular functor. This means roughly that regular epis are pullback stable. It is also supposed that some or all finite limits exist, depending on who you read. Suppose all, for simplicity. Also U preserves regular epis. Let \G denote the resultant cotriple on *A*. Now Beck showed that in all situations that the idea of A-module (A being an object of *A*) had been defined, it had a uniform description as an abelian group object in the slice *A*/A. So we set Mod(A) = Ab(*A*/A). What this does is to identify an A-module with the split extension over A with the module as kernel. If you do that, then for B --> A, the homset in *A*/A of B to M is simply Der(B,M). It therefore makes sense to call an adjoint (if it exists) to the inclusion Mod(A) --> *A*/A the modules of differentials Diff^A(B). I will assume it does exist for each object A. Corresponding to B --> A, there is a functor f_!:*A*/B --> *A*/A and it has a right adjoint f^* = A x_B -. This induces a functor, also called f^*:Mod(A) --> Mod(B) and, under mild conditions, that has a left adjoint f_#. That is usually tensoring with an enveloping object. Next assume given a chain complex functor C_*^A:*A*/A --> Mod(A) for each object A. Suppose that f_# takes C_*^B(C) to C_*^A(C) for an arrow C --> B. (Actually need that assumption only for C = B, but the more general case is what actually happens.) That is all background. Now come the three hypotheses that matter: 1. Assume that C_*(A) is a projective resolution of Diff^A(A). (This is the assumption that fails in the category of commutative algebras.) 2. Assume that UG^nA is projective in *X* for all n >= 0. 3. Assume that for each n >= 0, the functor C_n^A factors through U. More precisely, suppose that there is a functor ~C_n^A:*X*/UA --> Mod(A) such that C_n^A is naturally equivalent to the composite U/A ~C_n^A *A*/A --------> *X*/UA ---------> Mod(A) The conclusion is that the complexes C_*^A(A) is chain homotopic to the cotriple complex that has in degree n the module Diff^A(G^{n+1}A) with boundary induced in the usual way by the simplicial face operators. It is a formidable set of conditions, but of course, they are all readily satisfied in the cohomology theories in Cartan-Eilenberg. 1. essentially defines the C-E theory, 2. is obvious for group and associative algebra cohomology of an algebra projective over its ground ring, and is true (although non-trivially so) for a lie algebra that is projective over its ground ring. 3. has often been remarked and the fact that it plays a role was understood already in the original Barr-Beck paper. It says essentially that the algebra structure is not used in defining the C_n, only in defining the boundary operator. Michael ============================================================================== Subj: Atish Bagchi's address Date: 21 Oct 92 11:02:02 EDT From: Charles Wells The recent abstract of joint work by Atish Bagchi and me contained an erroneous email address for Atish: It should be axb32@po.cwru.edu. However, Atish will not be getting his email for a couple of weeks since he is out of the country. We hope he will return by early November. -- Charles Wells Department of Mathematics, Case Western Reserve University University Circle, Cleveland, OH 44106-7058, USA 216 368 2893 ============================================================================== Subj: tanglerads Date: Fri, 23 Oct 92 07:10:12 GMT-0400 From: jds@rademacher.math.upenn.edu Operads are a useful way of encoding compositions of maps from n variables to 1, modelled on grafting of trees - root to branchtip and as such appear e.g. in ``classical'' closed string field theory Qunatum corrections require a generalization for which the model should be the category of tangles or some such Any work been done on such a generalization? jim stasheff ============================================================================== Subj: Re: tanglerads Date: Sun, 25 Oct 92 10:36:37 +0100 From: Dip. Mat. - visitatore Jim Stasheff and a few others have a copy of old 1972 notes of mine on operads, essentially studying, besides the obvious convolution tensor product on the functor category [P,V], another derived one, the monads for which generalize Peter May's operads. Here P is the category of natural numbers and permutations while V is any symmetric monoidal closed category (complete and cocomplete). The case V = Set is familiar from Joyal's species. Suppose we replace P here by the braid category B; everything still seems to work, at a first brief glance; so we have a notion of B-operad. Is this what Jim is asking for? Max Kelly. ============================================================================== Subj: a question on categories of contexts (CS) From: koslowj@math.ksu.edu (Juergen Koslowski) Date: Mon, 26 Oct 92 14:00:34 CST This question concerns Bart Jacobs' paper "Simply typed and untyped Lambda Calculus revisited", in "Applications of Categories in Computer Science", Durham Proceedings, London Mathematical Society Lecture Note Series No. 177 In Example 3.2, Bart Jacobs constructs a term model for a certain kind of fibration (or indexed category). The base category has contexts as objects, i.e., finite tuples of type declarations, while morphisms are finite tuples of (beta-eta-equivalence classes of) terms. I have some trouble seeing that this category has finite products, given by concatenation of contexts, as claimed. Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I don't know whether Bart Jacobs has access to the net; maybe someone can forward this question to him? Thank you. regards, J"urgen -- J"urgen Koslowski | If I don't see you no more in this world Department of Mathematics | I meet you in the next world Kansas State University | and don't be late! koslowj@math.ksu.edu | Jimi Hendrix (Voodoo Chile) ============================================================================== Subj: Re: a question on categories of contexts (CS) From: alti@dcs.ed.ac.uk Date: Tue, 27 Oct 92 10:26:06 GMT Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I haven't read the paper in question but I can comment on this. In most presentations of typed \lambda calculi (e.g. Barendregt's PTS) this case (repeated use of the same variable) is excluded. Indeed it does not matter for the expressibility of the system because we can always consistently rename variables (\alpha conversion). Actually I prefer to use deBruijn indizes anyway. The translation of named variables into those indizes is certainly a matter for people writing compilers (i.e. handling a symbol table) but it should not be confused with the \lambda calculus. This two issues can and should be treated completeley seperately. DeBruijn indizes precisely correspond to projections and the usual operations of substitution and weakening have nice categorical explanations. Named variables are a complete redherring. Thorsten Altenkirch And there's a hand, my trusty fiere, Laboratory for Foundations And gie's a hand o' thine, of Computer Science And we'll tak a right guid-willie waught University of Edinburgh For auld lang syne! ============================================================================== Subj: categories of contexts From: Paul Taylor Date: Wed, 28 Oct 1992 12:12:05 +0000 Thorsten Altenkirch says > Named variables are a complete redherring. Named variables are the way that human mathematicians have been notating their work for centuries, and human programmers prefer them too. Even categorists give up \pi_1 and \pi_2 shortly after introducing the universal property of products! Thorsten also mentioned alpha conversion. There's an important distinction to be made with alpha conversion which corresponds to that between free (open) and bound (closed) variables. The closed term $\lambda x.x$ is to all intents and purposes the same as $\lambda y.y$ (and with de Bruijn indices *is* the same) but the open terms are quite different. My personal way of formulating this construction is as follows: * the objects are (finite) sets of distinct variable names together with their types, ie contexts; [x1:x1,x2:X2,...,xn:Xn] changing the names gives a different object * the morphisms are substitutions: [y1:=u1,y2:=u2,...,ym:=um] [x1:X1,x2:X2,...xn:Xn] ---------------------------> [y1:Y1,...,ym:Ym] where there's one "assignment" for each variable in the target context and the terms have their variables amongst those in the source. * composition is given right to left by the notationally simple rule [z:=v(y)] o [y:=u(x)] = [z:=v[y:=u]] I missed something out in the definition of morphism: I define *two* categories, one ("raw terms") consisting of closed-alpha equivalence classes, the other ("terms") being its quotient by beta/eta/etc equivalence. Similar constructions may be done for languages other than the simply typed lambda calculus. In fact lambda abstraction is not relevant to the issue. Now we may ask some elementary categorical questions: What are the isomorphisms in the category of *raw* terms? They are exactly the open alpha equivalences. In particular a context with two variables of the same type has a non-trivial automorphism. What do we get from concatenating two contexts which share no variable name? Assuming that the language admits individual variables as terms, allowing omission (weakening) and repetition (contraction), we obtain a product diagram. How can we form the product of contexts which do share variables, in particular the square of a context? We replace one or both by isomorphic copies (along open-alpha equivalences, ie renaming variables) and take the product of those. It seems to me that for any purpose other than the machine implementation of a compiler it is notationally better *not* to adopt a convention for consistently renaming variables in order to provide a canonical product in all cases. The product always *exists*, as I have shown (so long as we have an inexhaustible supply of new variable names), and there is a canonical choice of it, albeit involving an exception. If you're worried about the constructivity of the exception, remember that the variable names must have been chosen from amongst a decidable population, because I began by saying that they were distinct in each context (object). Paul Taylor ============================================================================== Subj: Re: a question on categories of contexts (CS) Date: Wed, 28 Oct 92 11:11:39 +0100 From: bjacobs@math.ruu.nl (Bart Jacobs) Reply to a question by J"urgen Koslowski (from 26 Oct 92). In logic and type theory, variables are there for human convenience. They are just pointers, which are given names. Such names are often used `locally' (i.e. in a specific term or formula) with an implicit convention that there are no `global' name clashes. Category theory provides a variable-free formalism for logics and type theories. One uses projections instead of variables. Things become more precise, but less readable. In constructing categories from syntax (as I did in Example 3.2 of my Durham 1991 paper in LMS 177, to which J"urgen refers), one can either use a very precise syntax (e.g. with de Bruijn indices) or be very sloppy and hope the reader is willing to understand things in the appropriate way. Clearly I have chosen the latter approach. Below is a syntax for variables and contexts in simply typed lambda calculus, which solves the problems mentioned by J"urgen. It is not the syntax which is used in practice, but it is still readable. I'll use semi-LaTeX and write the letters `s' and `t' for types \sigma and \tau and `G' and `D' for contexts \Gamma and \Delta. Fix an infinite set Var = {v_1, v_2, v_3,...} of variables. A context is defined to be a finite sequence of types written as G = v_1:s_1, ..., v_n:s_n where by convention one counts the variables starting from 1. Assume another context D = v_1:t_1, ..., v_m:t_m then the concatenation G,D is defined to be G,D = v_1:s_1, ..., v_n:s_n, v_n+1:t_1, ..., v_n+m:t_m In this way no variable clashes occur (and hence no overwriting). The projections are the (equivalence classes of the) sequences (v_1,...,v_n) : G,D --> G (v_n+1,...,v_n+m) : G,D --> D This makes G,D the cartesian product of contexts G and D in the base category of contexts in Example 3.2 in loc. cit. I assume J"urgen now wants to know the rules for handling such `canonical contexts'. Here they are. PROJECTION ---------------- v_1:s |- v_1:s WEAKENING G |- M:t ---------------- G,v_n:s |- M:t (where G is supposed to be of length n-1) CONTRACTION G,v_n:s,v_n+1:s |- M:t --------------------------- G,v_n:s |- M[v_n/v_n+1]:t EXCHANGE G,v_i:s_i,v_i+1:s_i+1,D |- M:t ----------------------------------------------------- G,v_i:s_i+1,v_i+1:s_i,D |- M[v_i/v_i+1,v_i+1/v_i]:t Using such a precise syntax the problem raised by J"urgen can be solved. I did not put it in the paper because I thought it would distract too much. Bart Jacobs. Address since Aug.1, 1992: Mathematical Institute, RUU P.O.Box 80.010 3508 TA Utrecht The Netherlands Email: bjacobs@math.ruu.nl ============================================================================== Subj: Re: categories of contexts Date: Thu, 29 Oct 1992 09:59:30 +0100 From: F.J.de.Vries@cwi.nl Dear Thorsten, :-)When proving properties about systems with bound variables it :-)simplifies notation and understandibility quite a lot when we use :-)de Bruijn's notation. Otherwise we end up mumbling the words "up to :-)alpha equivalence" like a mantra. Completely right, but you run the risk that for the outsider your remark that actually you use de Bruijn's notation may be interpreted as a mantra as well. :-)Recently I did a machine checked and complete formalisation of the :-)strong normalisation proof for System F using de Bruijn indices (LFCS :-)report 92-230). I find it very hard to imagine doing the same thing :-)with named variables. Indeed! I am intersted in receiving a copy of your report. What were the difficulties you encountered in making this machine checked proof? Did it take you a long time? many thanks in advance! (uuencoded dvi-version is also welcome...) Fer-Jan de Vries, Department of Software technology CWI Kruislaan 413 1098 SJ Amsterdam ferjan@cwi.nl ============================================================================== Subj: position announcement Date: Thu, 29 Oct 1992 14:41:11 +0100 From: David Murphy The following position has become available as a result of the award of an SERC fellowship for two years. Applicants with research interests in concurrency theory or categorical semantics are particularly welcomed. Further details are available from me or from the head of school: Professor Aaron Sloman School of Computer Science The University of Birmingham Edgbaston Birmingham B15 2TT England Email: A.Sloman@bham.ac.uk Phone: +44 (0)21 414 3711 Fax: +44 (0)21 414 4281 Thank you for your attention. David Murphy TEMPORARY LECTURESHIP IN COMPUTER SCIENCE The University of Birmingham ----------------------------------------- Post Reference: S1788/92A Starting Salary: On the scale pounds 13,400 - 18,576 a year (Plus superannuation.) Starting date: From April 1993 Closing date for receipt of applications: 19 November 1992 (It may be possible to consider applications received after the closing date if the selection process has not gone too far.) Application forms available from: The Director of Staffing Services The University of Birmingham Edgbaston Birmingham B15 2TT England Fax: +44 (0)21-414-4802 Telephone: +44 (0)21-414-6486 Further information ------------------- Applicants for the temporary lectureship should, ideally, have a PhD, or expect to have passed the examination by April 1993. In exceptional circumstances it may be decided to appoint someone without a PhD. Applicants for the temporary lectureship in Computer Science should have qualifications and a research record in some area of Computer Science or Software Engineering. It is expected that the lecturer will contribute to research, and research achievements and potential will play a strong role in the selection process. The initial need is for someone who can help with a course on data structures (and some teaching in C++), as well as project supervision for undergraduates and MSc students. It may be possible to rearrange teaching to suit the qualifications of the successful candidate. All applications should, if possible, include the applicant's home and office phone numbers, electronic mail address, names of referees, full information about the applicant's research interests and future research plans, areas of teaching expertise, and details of any relevant experience. It is helpful if phone numbers and electronic mail addresses of referees can be provided in case we need to make contact with them quickly.