Date: Tue, 3 Jan 1995 15:07:33 -0400 (AST) Subject: Re: composition of enriched functors Date: Mon, 2 Jan 95 09:34:16 +1100 From: Max Kelly David Yetter, in his query, seems to be making heavy weather of the composition of enriched functors. The composite of F:A --> B and G:B --> C is given on objects by GFa, while its "effect on maps" is the composite of the effects of F and of G as in A(a,a') ------> B(Fa,Fa') -----> C(GFa,GFa'). That is all. There is further a composition of profunctors (also called bimodules, or just modules), given by an evident co-end formula. Now every functor F determines a profunctor F*, where F*(a,b) is B(Fa,b); and the calculation David refers to (which is a simple application of the Yoneda isomorphism) is just the verification that (GF)* is canonically isomorphic to (G*)(F*). Of course this holds, in particular, for C-linear categories. New-Year greetings to all - Max Kelly. Date: Tue, 3 Jan 1995 15:09:26 -0400 (AST) Subject: David Yetter's question Date: Tue, 3 Jan 1995 14:43:10 +1100 From: Ross Street >The composition of F and G is then given by > > \integral^c Hom(F(-),c) \otimes Hom(G(c),-) \cong Hom(G(F(-)),-). This follows from the enriched Yoneda Lemma. The setting is as follows. It is tensor product of (bi)modules which is given by the coend formula. Modules (= profunctors = distributors) between V-categories are the arrows for a bicategory Mod(V) with this tensor product as composition. Each V-functor F becomes a module in two ways: F_* and F^*. The latter involves the Hom(F(a),c) as required by David. Each process gives a locally fully faithful embedding of V-Cat in V-Mod (Yoneda's Lemma) with appropriate variances. Moreover, F^* is right adjoint to F_* in the bicategory Mod(V). A good reference is Lawvere's paper "Metric spaces, generalised logic, and closed categories" Rend. Sem. Mat. Fis. Milano 43 (1974) 135-166. Best wishes for the New Year, Ross Date: Fri, 6 Jan 1995 19:36:50 -0400 (AST) Subject: Electronic Journal on Category Theory Date: Fri, 6 Jan 1995 19:31:49 -0400 (AST) From: Bob Rosebrugh ANNOUNCEMENT AND CALL FOR PAPERS This is announce a new refereed electronic journal THEORY AND APPLICATIONS OF CATEGORIES The Editors, who are listed below, invite submission of articles for publication in the first volume (1995) of the journal. The Editorial Policy of the journal, basic information about subscribing and some information for authors follows. More details are available from the journal's WWW server at URL http://www.tac.mta.ca/tac/ or by anonymous ftp from ftp.tac.mta.ca in the directory pub/tac. EDITORIAL POLICY The journal Theory and Applications of Categories will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. The method of distribution of the journal is via the Internet tools WWW/gopher/ftp. The journal is archived electronically and in printed paper format. SUBSCRIPTION INFORMATION Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi and Postscript format. Details will be e-mailed to new subscribers and are available by WWW/gopher/ftp. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, INFORMATION FOR AUTHORS The typesetting language of the journal is TeX, and LaTeX is the preferred flavour. TeX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. Please obtain detailed information on submission format and style files by WWW or anonymous ftp from the sites listed above. You may also write to tac@mta.ca to receive details by e-mail. EDITORIAL BOARD John Baez, University of California, Riverside baez@math.ucr.edu Michael Barr, McGill University barr@triples.math.mcgill.ca Lawrence Breen, Universite de Paris 13 breen@math.univ-paris.fr Ronald Brown, University of North Wales r.brown@bangor.ac.ik Jean-Luc Brylinski, Pennsylvania State University jlb@math.psu.edu Aurelio Carboni, University of Genoa carboni@vmimat.mat.unimi.it G. Max Kelly, University of Sydney kelly_m@maths.su.oz.au Anders Kock, University of Aarhus kock@mi.aau.dk F. William Lawvere, State University of New York at Buffalo mthfwl@ubvms.cc.buffalo.edu Jean-Louis Loday, Universite de Strasbourg loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht moerdijk@math.ruu.nl Susan Niefield, Union College niefiels@gar.union.edu Robert Pare, Dalhousie University pare@cs.dal.ca Andrew Pitts, University of Cambridge ap@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University rrosebrugh@mta.ca Jiri Rosicky, Masaryk University rosicky@math.muni.cz James Stasheff, University of North Carolina jds@charlie.math.unc.edu Ross Street, Macquarie University street@macadam.mpce.mq.edu.au Walter Tholen, York University tholen@vm1.yorku.ca R. W. Thomason, Universite de Paris 7 thomason@mathp7.jussieu.fr Myles Tierney, Rutgers University tierney@math.rutgers.edu Robert F. C. Walters, University of Sydney walters_b@maths.su.oz.au R. J. Wood, Dalhousie University rjwood@cs.da.ca Date: Fri, 6 Jan 1995 23:10:21 -0400 (AST) Subject: 1. ctrc.html 2. Tensor and Linear Time Date: Fri, 6 Jan 1995 16:52:40 -0500 From: Jim Otto Dear People 1. There is now a small web page at URL ftp://triples.math.mcgill.ca/ctrc.html for the Centre de Recherche en Th'eorie des Cat'egories -- Montr'eal. 2. Linked to that web page is my web page and linked to my web page is an expanded and corrected paper on linear time, whose introduction is below. Bon Jour, J. Otto Tensor and Linear Time Introduction Quite simply, serial composition is <--- <--- while parallel composition = tensor is <--- <--- even though we will run both sequentially (section 4.6). Tensor, rather than product, not only provides more models [Huwig 82], but may be necessary at tier 0 in order to avoid the diagonal bug (section 4.6). Roughly, tier 0 is what may go inside loops, while tier 1 is what is defined by loops (section 4.1). By the way, 0-ary serial composition = the identities, while 0-ary parallel composition = the unit. The main text consists of sections 1. Almost Equational Specification, 2. Tensor and System T, 3. Comprehensions and Tiers, 4. Linear Time, and 5. The Linear Time Hierarchy. Section 4 characterizes the linear time functions, using ideas from [Bellantoni-Cook 92, Bloch 92, Leivant-Marion 92], and provides a formal system for them. Section 5 characterizes, improving [Wrathall 78], the linear time hierarchy relations. (These are the Delta_0 relations [H'ajek-Pudl'ak 93, Woods 86].) Section 1, using ideas from [Makkai 94, Ad'amek-Rosick'y 94], explains the almost equational specification which we use throughout. It is based on 2 layers of restricted equational specification: sketches and orthogonality. Section 2 specifies the idealized, but unfeasible, recursion of G"odel's system T, while section 3 provides a means, namely comprehensions and tiers, to attain feasibility. Technical issues have been pushed to the appendices, which are A. Sketches as Presheaves, B. Initial Models, C. Coherence, D. Linear Implication, E. Cotensor, F. Gluing, and G. Turing machines. The main text is hopefully generally readable with perhaps a few glances at say [Barr-Wells 90, 85]. We have used latex2e, xy-pic, and auc-tex. Date: Mon, 9 Jan 1995 08:20:51 -0400 (AST) Subject: Re: composition of enriched functors Date: Mon, 9 Jan 1995 09:02:15 +0100 From: Axel Poigne Referring to recent contibutions by Yetter and Kelly. As remarked by Kelly, the construction is straightforward. A paper strongly recommended to be read in this context is Lawvere's 'Generalized Metric Spaces ...". The material about composition of profunctors + construction of "free algebras" are to be found in my contribution "Basic category theory", chpt. 6, in the Handbook of Logic in Computer Science (Abramsky, Gabbay, Maibaum, eds.). Axel Poigne Date: Mon, 9 Jan 1995 08:24:15 -0400 (AST) Subject: Re: question on cHa's Date: Mon, 9 Jan 1995 12:16:16 +0000 From: Steven Vickers >Does somebody know whether for a complete Heyting algebra (cHa) A >such that the specialization order on points is discrete it >automatically holds whether for ALL cHa's B the frame morphisms >from A to B are ordered discretely by the spezialization order. >I know that there are cases (different from complete Boolean >algebras) where it holds but does it hold in general ? > >Thomas Streicher It's not true. I expect there are already lots of counterexamples amongst non-trivial pointless locales, but here's something more straightforward. Let D be a non-trivial locale with no global points (global point = locale map from 1 to D) and let D' be its lift (or localification), which has a new bottom point adjoined - by adjoining a new top to its frame. D' has only one global point (the new bottom) and so the specialization order on global points is discrete. However, we have two generalized points of D' at stage D' itself (locale maps from D' to D'), namely the generic point id: D' -> D' and the bottom _|_: D' -> 1 -> D', and they are distinct with _|_ <= id. Steve Vickers. Date: Tue, 10 Jan 1995 00:26:05 -0400 (AST) Subject: Tools for cat theory: Using ftp rather than mosaic. Date: Mon, 9 Jan 1995 11:17:48 -0500 From: Jim Otto To: stone@math.ubc.ca Hi. Coming in using ftp I don't find anything I can "get" (that seems to be related to your Tensor and Linear Time paper.) Perhaps I should learn something about "crtc.html". Can you suggest what command I should begin with (using what's essentially BSD 4.3 on a dept. NeXT to which I'm connected via modem and phone line ((to another NeXT on my desk)) ) ? I've been trying "appropos" with everything I can think of, like "ctrc" and "html", but so far with no hits. Art Dear Art Stone So my directions on
  • Centre de Recherche en Thiorie des Catigories -- Montrial. were too implicit. To use ftp rather than say mosaic 1. Do anonymous ftp to triples.math.mcgill.ca 2. get ctrc.html By the way, it's not according to the French spelling or the Canadian version of the American FCC, but rather the English spelling `Category Theory Research Center'. 3. Read that J. Otto is at pub/otto/otto.html
  • J. Otto 4. cd pub/otto and then get otto.html 5. Read that the new paper is at c-docs/tensor.ps.gz New papers on complexity doctrines.
    • Tensor and Liner Time (42 pages). Submitted to the proceedings of the workshop on logic and computational complexity.
    6. cd c-docs and get tensor.ps.gz 7. If you don't have gunzip, get it from say the GNU directory on gatekeeper as pointed to by otto.html.
  • Gatekeeper. Well actually that one won't work for ftp. This one will
  • GNU Or get someone to setup a web previewer, say mosaic, and its utilities, especially gunzip, gs, and ghostview. O'Reilly has a nice book on mosaic.
  • O'Reilly & Associates, Inc. So, just as .bib's are useful even without bibtex, .html's are useful without mosaic, lynx, or WWW. On the other hand, newer software can make guru mumbo jumbo a no-brainer. Bon Jour, J. Otto Date: Tue, 10 Jan 1995 12:52:34 -0400 (AST) Subject: algebraically compact categories Date: Tue, 10 Jan 1995 11:05:10 -0500 From: Peter Freyd When I first introduced the notions of algebraically complete categories (every endo-functor has an initial algebra) and algebraically compact categories (every endo-functor has an initial algebra naturally isomorphic to a terminal co-algebra) I thought that such things would exist in the classical foundations only in degenerate form. It was a surprise when I noticed that the categories of countable sets and of countably dimensioned vector spaces are algebraically complete. I'm now surprised by: The category of separable Hilbert spaces and linear operators of bound at most 1 is algebraically compact. As in the earlier cases one doesn't really need the controlling cardinal number to be aleph-naught. To avoid using the axiom of choice one can state the more general result by taking an arbitrary Hilbert space A and defining *A* by: Objects of *A*: all those Hilbert spaces that can be isometrically embedded in A; Maps of *A*: all linear operators thereon of bound at most 1. Then: *A* is algebraically compact. The theorem holds for both the real and complex cases. In the proof I use the surprising (to me) fact that in the categories in question every half-invertible map has a _unique_ half-inverse. (That is, every map has at most one left-inverse and one right- inverse.) All the other examples from nature that I can think of are categories in which the only half-invertibles are invertible. Are there others? Peter Freyd Date: Fri, 13 Jan 1995 19:34:31 -0400 (AST) Subject: Book on Curry-Howard Isomorphism Date: 13 Jan 1995 20:01:02 GMT From: Charles Wells I believe there is a new book out on the Curry-Howard Isomorphism, but I have lost the announcement. If someone can give me the details, I would like to order it for the CWRU library. Thanks, -- Charles Wells Department of Mathematics, Case Western Reserve University 10900 Euclid Avenue, Cleveland, OH 44106-7058, USA 216 368 2893 Date: Sat, 14 Jan 1995 09:33:12 -0400 (AST) Subject: Hilbert space proof Date: Sat, 14 Jan 1995 07:47:49 -0500 From: Peter Freyd On request: Theorem: The category of separable Hilbert spaces and linear operators of bound at most 1 is algebraically compact. More generally, Theorem: Let A be a Hilbert space. Let *A* be the category whose objects are all Hilbert spaces that can be isometrically embedded in A and whose maps are all linear operators therebetween of bound at most 1. Then *A* is algebraically compact. (The axiom of choice says that the objects of *A* can be described as all Hilbert spaces of (orthonormal) dimension bounded by a given cardinal.) The proofs work for both the real and complex cases. For the proof we'll need a few lemmas about *A* and its endofunctors. First note that any isometric embedding B -> C is a retract with the adjoint operator C -> B serving as its right- inverse. Left to the reader is the surprising fact (to me) that right- inverses are unique. So are left-inverses. That is, in *A* every map has at most one right-inverse and one left-inverse and all left- inverses are isometric embeddings and all right-inverses are orthogonal projections. Because any functor preserves the existence of right-inverses we may conclude that any given endofunctor, T, carries isometric embeddings to isometric embeddings. For convenience we'll replace T with a naturally equivalent functor that is invariant on the lattice of subobjects of A (that is, the subcategory of all closed subspaces of A and all inclusion maps therebetween). First choose a single isometric embedding TA -> A. For each A' contained in A define T'A' to be the image of TA' -> TA -> A where TA' -> TA is T applied to the inclusion map A' -> A. Let TA' -> T'A' be the obvious isomorphism. For all objects, B, not contained in A define T'B to be TB and TB -> T'B to be the identity map. Define T' to be the unique endofunctor that turns this collection of isomorphisms into a natural equivalence. For an inclusion map A' -> A we have that T'A' -> T'A is an inclusion map. And from that we may conclude that any inclusion map between subobjects of A is carried by T' to an inclusion map. We'll drop the dash-mark on T and notationally assume that our given functor preserves the lattice of subobjects of A. At this point it is clear (a la Tarski) what the initial T-algebra must be: any endofunctor on a complete lattice has a minimal fixed point, indeed, to domain theorists (a CS term) it is clear how to prove it to be the initial T-algebra: start by using the bottom-up construction for the minimal fixed-point for T as it operates on the lattice of subobjects of A. Define an ordinal sequence of subspaces of A as follows: for a limit ordinal 'a, take F['a] to be the supremum of the previous values; for a successor ordinal 1+'b take F[1+'b] to be T(F['b]). Note that for the limit ordinal 0 we have that F[0] is the trivial (one-element) subspace. And note that for all other limit ordinals, 'a, we have that F['a] is the closure of the union of the previous values. By an inductive argument this sequence is an increasing sequence (but, of course, not forever strictly increasing): for a limit ordinal 'a, we have that F['b] < F['a] for all 'b < 'a (using < for the containment sign) hence T(F['b]) < T(F['a]) that is, F[1+'b] < F[1+'a] for all 'b < 'a and the construction of F['a] forces F['a] < T(F['a]) = F[1+'a]; for a successor ordinal 1+'b we may (inductively) assume that F['b] < F[1+'b] hence T(F['b]) < T(F[1+'b]), that is, F[1+'b] < F[1+1+'b]. The sequence can not forever be strictly increasing. It stabilizes at a value F. We take 'c as the first limit ordinal such that F = F['c]. We need that F is not just the supremum of the constructing sequence as defined in the lattice but its colimit as defined in the entire category. Actually we need the general fact that for any limit ordinal 'a it is the case that F['a] is the colimit of the ordinal diagram of previous values. The proof is straigh- forward using again the fact that the maps in the category are of bound at most 1.) Given a T-algebra b:TB -> B we must construct a map x:F -> B so that F Tx / \ x TB -> B b (add downward arrowheads). We define, inductively, a sequence of maps x['b]:F['b] -> B such that x['b] T(x['b]) b F['b] -----> B = F['b] -> F[1+'b] --------> FB -> B where the unlabeled map is the inclusion map. For successor-ordinals define x[1+'b] as T(x['b]) b F[1+'b] --------> FB -> B. The inductive verification that x[1+'b] T(x[1+'b]) b F[1+'b] -------> B = F[1+'b] -> F[1+1+'b] ----------> FB -> B is straight-forward diagram chasing. For limit-ordinals define x['a]:F['a] -> B using the fact that F['a] is a colimit of the previous values. For the verification of x['a] T(x['a]) b F['a] -----> B = F['a] -> F[1+'a] --------> FB -> B it suffices to verify, for each 'b < 'a, that x['a] T(x['a]) b F['b] -> F['a] -----> B = F['b] -> F['a] -> F[1+'a] --------> FB -> B where, just as before, each unlabeled arrow is an inclusion map. This follows, inductively, from the two equations x['a] x['b] F['b] -> F['a] -----> B = F['b] -----> B, and F['b] -> F['a] -> F[1+'a] = F['b] -> F[1+'b] -> F[1+'a] where the last map (still an inclusion map) is the result of applying T to the inclusion map from F['b] to F['a]. The uniqueness can be verified, inductively, for each 'b. Alternatively, given a possibly different solution y:F -> B, let A' be the equalizer of x and y using the standard construction: A' is the closed subspace of points on which x and y agree. It follows that T(A') is contained in A', that is, A' is a "prefixed point" of T. But -- as is clear from the top-down construction -- minimal fixed points are automatically minimal prefixed points and F must be contained in A'. We have shown that T has an initial algebra (that is, the category is algebraically complete). Since the category is self-dual (via the adjoint-operator construction) it follows that T also has a final co-algebra (that is, the category is algebraically co-complete). But for compactness we need the two to be naturally isomorphic. We have reduced to the case that the structure map on the initial algebra is the identity map which means that the naturally isomorphic co-algebra is given by the same identity map. That is, we must show for every b:B -> TB the existence of a unique x:B -> F such that (add downward arrowheads) b B -> TB x \ / Tx F. F is not just the colimit of the ordinal sequence of inclusion maps, it's the limit of the ordinal sequence of their adjoint operators, the orthogonal projections. The comments at the very beginning, that T necessarily preserves the unique right-inverses, says that this ordinal sequence of orthogonal projections has all the requisite properties for the (dual) of the proof we've just seen. Done. Having done all this I must now note that my original purpose for algebraic compactness has been frustrated: the fact that contravariant functors and mixed-variance functors have minimal invariant objects was already evident for this category. I'm refering to the general theorem that given any algebraically compact category and "sesqui"- endofunctor, TXY, contravariant on X, covariant on Y, there's a T-invariant object, that is, an object F together with an isomorphism from TFF to F; indeed there is a _minimal_ T-invariant object, that is, one that appears uniquely as a natural retract of every T-invariant object. The trouble is that if we replace TXY with TX'Y, where X' denotes the adjoint-operator functor (which, note, is the identity operation on objects) then it's easy to see that the intial algebra of TX'Y is as desired. That is, algebraic completeness is enough when in the presence of an anti-involution that fixes identity maps. Peter Freyd Date: Mon, 16 Jan 1995 22:11:24 -0400 (AST) Subject: is union associative? Date: Sat, 14 Jan 1995 15:09:39 +0000 (GMT) From: Ilya Beylin I suspect that the following question is very natural and a known solution has to exist, but I cannot find any reference in books I have. Consider the following diagram A |a V b W <----- B and define union of two morphisms a U b := Pushout(Pullback(X)) In the category Set this operation is obviously associative: for any arrows a,b,c with common target, a U (b U c) = (a U b) U c , Can anybody tell, what conditions should be imposed to a category to guarantee this associativity? Thank you in advance, Ilya Beylin Date: Mon, 16 Jan 1995 22:15:12 -0400 (AST) Subject: Re: Hilbert space proof Date: Sat, 14 Jan 95 15:26:17 EST From: Michael Barr I haven't checked the precise claim, but I think that what Peter claims is in my paper in JPAA in 1992 called Algebraically Compact Functors. The paper was, if I recall correctly, transmitted by guess who. Actually, Peter asked me in 1990 when I was leave at Penn if this were true. The paper is also available for ftp (don't tell North-Holland). I haven't studied Peter's argument, so I don't know how much it differs from mine. Actually, I haven't look at mine in several years either. A similar category, with a similar result is that of sets are injective partial functions. Interestingly, if you want to know on what category it is natural to define l^2 as a functor, it is sets and partial injections. Michael Date: Tue, 17 Jan 1995 09:32:59 -0400 (AST) Subject: Re: Hilbert space proof Date: Mon, 16 Jan 1995 19:07:54 +0000 (GMT) From: Samson Abramsky Peter, Do you have any interesting examples of ``domain equations'' over this category? There is certainly no model of the lambda calculus there. Samson Date: Tue, 17 Jan 1995 09:35:59 -0400 (AST) Subject: neologism To: cat-dist@mta.ca Subject: neologism In answer to the obvious query: yes, I did indeed check the standard sources before I let that word pass. And I decided the standard sources need to be improved. Now I must agree we've lived all these years without feeling the need for yet another adverb that starts out with "there-". The O.E.D. lists 38 of them: thereabout, thereabove, thereafter, thereafterward, thereagain, thereagainst, thereamong, thereat, thereaway, therebefore, therebeside, thereby, theredown, thereforth, therefrom, therehence, therein, thereinto, there-nigh, thereof, thereon, thereout, thereover, therethrough, theretill, thereto, theretofore, theretoward, thereunder, thereuntill, thereunto, thereup, thereupon, thereward, therewhile, therewith, therewithal, therewithin But none of these works as a replacement for "therebetween" in either of the following two lines from my recent missive: the category whose objects are all Hilbert spaces that can be isometrically embedded in A and whose maps are all linear operators therebetween of bound at most 1. the subcategory of all closed subspaces of A and all inclusion maps therebetween. So why not shoot for 39? Best thoughts, Peter Date: Tue, 17 Jan 1995 22:57:22 -0400 (AST) Subject: answer to Samson Date: Tue, 17 Jan 1995 08:58:28 -0500 From: Peter Freyd As my last paragraph tried to make clear, we can't expect much. If we define Hom(X,Y) as (adj X) tensor Y then the functor A directsum Hom(x,Y) looks as if it ought to have an interesting fixed point. It doesn't. Date: Fri, 20 Jan 1995 14:15:33 -0400 (AST) Subject: Re: is union associative? Date: Thu, 19 Jan 1995 13:47:09 -0500 From: Peter Freyd Subject: Re: is union associative? Ilya Beylin asked for which categories is union associative, where union is defined by: Consider the following diagram A |a V b W <----- B and define union of two morphisms a U b := Pushout(Pullback(X)) (I'm a little troubled with a non-idempotent operation being called a union.) It's true in any pre-topos. For a proof I would specialize to the case that W is the terminator (move to the slice category if it isn't). Let me use @ for the binary operation on isomorphism types characterized by the pushout diagram A x B / \ A B (add downward arrows) \ / A @ B (where it's understood that the top half is a product diagram}. Given a subobject X' in X recall that X/X' is characterized by the pushout X' / \ X Spt(X') \ / X/X' where Spt(X'), the support of X', is the image of X; -> 1. Then A @ B = (A + B)/(AxSpt(B) + Spt(A)xB)). Beyond the pre-topos case, I have no idea of just what's needed. For a counterexampe take the category of Z-sets (an object is a set with an automorphism) in which all orbits have three or fewer elements, take A to be a two-element orbit, B to be a three-element orbit. Then A @ (B @ B) is the terminator and (A @ B) @ B is isomoprhic to A + 1. (B @ B is the terminator and in any category 1 @ X = 1. A @ B is A + B.) Date: Wed, 25 Jan 1995 10:08:25 -0400 (AST) Subject: Preprint Available Date: Tue, 24 Jan 95 17:53:08 +1100 From: Walter Tholen The following paper may be requested from Maria Manuel Clementino (paper or electronic copy) by writing to clementino@gemini.ci.uc.pt "Compact objects and perfect morphisms" by M.M. Clementino, E. Giuli and W. Tholen Abstract: In a category with a subobject structure and a closure operator, we provide a categorical theory of compactness and perfectness which yields a number of classical results of general topology as special cases, including the product theorems by Tychonoff and Frolik and the existence of Stone-Cech compactifications, both for spaces and maps. Applications to other categories are also provided. Date: Wed, 25 Jan 1995 10:18:24 -0400 (AST) Subject: CT95 2'nd Announc't; Summer School on Category Theory Date: Wed, 25 Jan 1995 10:05:28 -0400 (AST) From: Bob Rosebrugh SECOND ANNOUNCEMENT INTERNATIONAL CATEGORY THEORY MEETING (CT95) Canadian Mathematical Society Annual Seminar July 9-15, 1995 Dalhousie University Halifax, Canada PREREGISTRATION IF YOU HAVE NOT ALREADY DONE SO, AND PLAN TO ATTEND THE CONFERENCE, PLEASE PREREGISTER BY FEBRUARY 15, 1995. To preregister, and thus receive detailed information, please send e-mail to ct95@cs.dal.ca with subject `preregistration'. Please provide your name and a postal address in the body of the message. (If you do not have access to e-mail, you may write to RJ Wood, Mathematics, Statistics and Computing Science, Dalhousie University, Halifax, Nova Scotia, B3H 3J5, CANADA.) REGISTRATION FEE The conference registration fee is $250(Canadian). Students may register for $125. The registration fee includes lunches during the days of the scientific program, an excursion and a banquet. Tickets for companions to attend any of the events will be available at cost. ACCOMMODATION To request residence accommodation at Dalhousie please send e-mail to ATANNER@KILCOM1.UCIS.DAL.CA mentioning CT95. (If you do not have access to e-mail, you may write to Conference Administrator, Conference Services, Dalhousie University, Suite 410, Student Union Building, Halifax, Nova Scotia, B3H 4J2, CANADA.) Rates, including taxes, are $35 nightly/$207 weekly for a single room, $51 nightly/$307 weekly for a double room. Breakfast is included with residence accommodation. Information on hotel accommodations will be included with a future mailing. SCIENTIFIC PROGRAMME Abstracts for talks should be sent to pare@cs.dal.ca (or R. Pare, Mathematics, Statistics and Computing Science, Dalhousie University, Halifax, Nova Scotia, B3H 3J5, CANADA) before May 1, 1995. ------------------------------------------------------------------------- FIRST ANNOUNCEMENT CATEGORY THEORY SUMMER SCHOOL June 25-July 8, 1995 Dalhousie University Halifax, Canada In conjunction with CT95, Professors F.W. Lawvere and S. Schanuel will be offering a series of preparatory lectures for graduate students who plan to attend the conference. There is no registration fee for this SUMMER SCHOOL. Student accommodation is $20 nightly/$110 weekly and should be requested from ATANNER@KILCOM1.UCIS.DAL.CA (or Conference Administrator, Conference Services, Dalhousie University, Suite 410, Student Union Building, Halifax, Nova Scotia, B3H 4J2, CANADA). Date: Mon, 30 Jan 1995 00:52:23 -0400 (AST) Subject: Announce: revision of paper Date: Fri, 27 Jan 95 11:28:56 EST From: Robert A. G. Seely We wish to announce the availability (by ftp or WWW) of the following paper (revised version) Natural deduction and coherence for weakly distributive categories by R.F. Blute, J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble ABSTRACT: This paper examines coherence for certain monoidal categories using techniques coming from the proof theory of linear logic, in particular making heavy use of the graphical techniques of proof nets. We define a two sided notion of proof net, suitable for categories like weakly distributive categories which have the two-tensor structure (times/par) of linear logic, but lack a negation operator. Representing morphisms in weakly distributive categories as such nets, we derive a coherence theorem for such categories. As part of this process, we develop a theory of expansion-reduction systems with equalities and a term calculus for proof nets, each of which is of independent interest. In the symmetric case the expansion reduction system on the term calculus yields a decision procedure for the equality of maps for free weakly distributive categories. The main results of this paper are these. First we have proved coherence for the full theory of weakly distributive categories, extending similar results for monoidal categories to include the treatment of the tensor units. Second, we extend these coherence results to the full theory of *-autonomous categories - providing a decision procedure for the maps of free symmetric *-autonomous categories. Third, we derive a conservative extension result for the passage from weakly distributive categories to *-autonomous categories. We show strong categorical conservativity, in the sense that the unit of the adjunction between weakly distributive and *-autonomous categories is fully faithful. NOTES: This is a significant revision of an earlier version announced a year ago. The paper has been completely rewritten, and has been enhanced in several ways: 1) We now treat the cases with non-logical axioms, and with non-commutative tensor and par, in considerable detail, pointing out in passing where the traditional treatment (of the pure commutative case) does not work in these cases. For example, the traditional proof of sequentiality (via splitting links) does not work in the presence of non-logical axioms. 2) We develop a term calculus for proof nets, and a theory of expansion - reduction rewrite systems, both of which are of independant interest. 3) Using this new material has made the proofs clearer and more complete. TO OBTAIN THE PAPER: By ftp: ftp triples.math.mcgill.ca login as anonymous use your email address as password cd pub/rags/nets binary get nets.ps.gz (or nets.dvi.gz if you prefer) (You will have to gunzip this file to get the PostScript - or DVI - file for the paper.) By WWW (Mosaic, netscape, ...) My home page is: ftp://triples.math.mcgill.ca/pub/rags/ragstriples.html click on the item labelled with the paper's title - this will display the PostScript file. (other papers dealing with weakly distributive categories and proof nets may be found easily via my home page.) (If you need to get gunzip, you can find it at pip.shsu.edu: issue the command "quote site index gzip" once you have ftp'd the site to get a list of files suitable for various computer platforms.) = rags = Date: Mon, 30 Jan 1995 00:55:19 -0400 (AST) Subject: Post-doc in Sydney Date: Sat, 28 Jan 1995 12:11:07 +1100 From: Barry Jay Subject: Post-doc in Sydney The SHAPE project ------------------ Post-doctoral Research Fellowship --------------------------------- The Shape project is developing some exciting new ideas in the semantics of data types so that they can be incorporated into programming languages, especially a parallel language suitable for numerical analysis. The key concept is that data is stored in shapes (or containers, or structures) which can be described and manipulated separately from the data. Expected benefits are: - that programs will be able to act on inputs of arbitrary shape (shape polymorphism); - that shape errors (e.g. array bound errors) can be detected during compilation (shape analysis), and; - that (most) run-time operations will act on arrays. Further information about the theory of shape can be obtained by anonymous ftp from ftp.socs.uts.edu.au in the directory users/cbj in the file shapelyTypes.ps.Z and the sub-directory P2. A prototype functional language is currently under development. When stable, it must be implemented so that it can run on the CM5. In addition to capturing the benefits listed above, shape information may help in optimisation. The UTS team currently has two staff and three graduate students, with additional collaborators in Australia, Canada and Europe. Now, with funding from a large ARC grant, we are looking for a post-doctoral research fellow. The position is for up to three years at a salary range of $42,198 - $43,781. A doctorate in computer science (or its equivalent) is essential. The candidate must be able to make a significant contribution to the project. The ideal candidate will have experience in implementing languages on parallel computers, optimisation of programs for parallel computers, functional programming, or; type theory. The candidate must have initiative, be able to work well as part of a team, and communicate effectively. Address initial enquiries to Barry Jay (cbj@socs.uts.edu.au). Responses may be erratic until 6/2/95. Applicants should send a curriculum vitae to: Dr C. Barry Jay School of Computing Sciences, University of Technology, Sydney PO Box 123 Broadway 2007 Australia Ph (6 12) 330-1814 Fax (6 12) 330-1807 before Friday, 24th February, 1995. The position will remain open until it is filled. Barry Jay