May 2003 - Categories - categories.org.au

More Topos questions ala "Conceptual Mathematics"
by Galchin Vasili 11 Jun '03

11 Jun '03

Hello, 1) In the very last chapter (Session 33 "2: Toposes and logic" of "Conceptual Mathematics" where the authors cover topoi, they define '=>' for the internal Heyting algebra of Omega: "Another logical operation is 'implication', which is denoted '=>'. This is also a map Omega x Omega->Omega, defined as the classifying map of the subobject S 'hook' Omega x Omega determined by the all those <alpha, beta> in Omega x Omega such that alpha "subset of" beta." Starting from "subobject S 'hook" ......" I got totally lost. I am frustrated because I know this is crucial to understanding why Omega is an internal Heyting algebra, so any help would be appreciated. (I am assuming that alpha and beta are subojects of Omega???). 2) In the same Session 33 on pg 350 is a set "rules of logic". These are exactly the axioms for a Heyting algebra, yes? Regards, Bill Halchin

2 2

Function composition of natural transformations? (Pat Donaly)
by Jpdonaly＠aol.com 09 Jun '03

09 Jun '03

Here is a technical/pedagogical question which has been bothering me for about twelve years. In problem 5 on page 19 of "Categories for the Working Mathematician" (CWM), Saunders Mac Lane points out that a natural transformation may be fully extended to an intertwining function from one category to another, intertwining meaning (except in the void case), that the function transforms on one side according to its domain functor and on the other according to its codomain functor. Then on page 42 Mac Lane introduces what he calls "horizontal" composition diagramatically and without reference to the fully extended intertwining functions. But the function composite of such a pair of functions trivially intertwines the function composite of the domain functors with that of the codomain functors, and this function composition operation is very quickly verified to be "horizontal" composition when written in terms of restrictions to sets of objects. Thus Mac Lane and everyone else I have read leaves the impression that an honest verification of, say, the associativity of "horizontal" composition would require a somewhat involved diagrammatic demonstration which, in fact, would be nothing other than the hard way to prove the associativity of function composition. Presumably this has been noticed for a long, long time, but the 1998 edition of CWM did not mention it, and I can't help but be struck by the fact that other authors' terminologies leave the impression that they don't know or don't care that "horizontal", star or Godement composition is function composition. Notationally, I am bemused to see the standard symbol for function composition (the small circle) degraded into a generic symbol for the composition of just about any category, while a star or an asterisk is frequently used to denote what amounts to function composition done awkwardly. This worries me that I am somehow overlooking something fairly blatant. Can someone tell me what it is? Jpdonaly(a)aol.com

2 1

Topos logic arises naturally
by Till Mossakowski 04 Jun '03

04 Jun '03

You see: even with just aesthetic and software engineering considerations you are eventually lead to topos logic... -- Till Mossakowski Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen till(a)tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till Message-Id: <200305270616.h4R6G3w8008134(a)plxc2089.pdx.intel.com> To: Randy Pollack <rap(a)inf.ed.ac.uk> cc: John Harrison <johnh(a)ichips.intel.com>, isabelle-users(a)cl.cam.ac.uk Subject: Re: HOL without description operators Date: Mon, 26 May 2003 23:16:03 -0700 From: John R Harrison <johnh(a)ichips.intel.com> Sender: Larry Paulson <Larry.Paulson(a)cl.cam.ac.uk> Hi Randy, | Perhaps more usefully, how do you suggest I do this task of developing HOL | without description operators. You might find it interesting to look at HOL Light. This gives a different axiomatization of the HOL logic, developed precisely because I was dissatisfied with the one in the original HOL system, on which I believe the Isabelle/HOL logic is based. Although I do eventually introduce the description operator, quite a lot of the basic logic --- including the automation of inductive definitions --- is developed without it (and indeed without excluded middle or extensionality). You may find it a more congenial starting-point. As Konrad Slind later pointed out, what I settled on is remarkably close to the internal logic of a topos, as presented for example in Lambek and Scott's book. This was a surprise to me since at that time I knew next to nothing about toposes and was motivated by a mixture of aesthetic and software engineering considerations. Cheers, John.

6 7

Semantic tableaux and intuitionistic logic
by Galchin Vasili 02 Jun '03

02 Jun '03

Hello, I am only familiar with semantic tableaux for classical propositional logic (and classical 1st order logic). It seems that as an inference system it is based squarely around the law of the excluded middle because it is essentially reductio ad absurdum. Hence, as an inference system it can't be simply modified for intuitionistic propositional calculus?? (Of course, I am bringing this because the role that Heyting algebras play in Topos theory). Regards, Bill Halchin

2 1

universal colimits in 2-cat
by Krzysztof Worytkiewicz 31 May '03

31 May '03

Dear All, Is anybody aware of a reference to the fact that small colimits are universal in 2-Cat ? Cheers Krzysztof

1 0

Injective Objects in a Category of coalgebras
by cat-dist＠mta.ca 29 May '03

29 May '03

Dear All, Do injective objects exist in the category of the coalgebras of the functor Po(Ax-) where P is the power set functor and A a non empty set? If the answer is yes, can they be characterized? Best regards. Maurice =3D=3D=3D=3D=3D A bientot. Maurice <kianpi maurice><mkianpi(a)uycdc.uninet.cm> ___________________________________________________________ Do You Yahoo!? -- Une adresse @yahoo.fr gratuite et en fran=E7ais ! Yahoo! Mail : http://fr.mail.yahoo.com

1 0

PSSL 79 - FINAL ANNOUNCEMENT
by Benno van den Berg 29 May '03

29 May '03

PSSL 79 - DOORN, THE NETHERLANDS - FINAL ANNOUNCEMENT Dear all, This is the final announcement for the 79th meeting of the Peripatetic Seminar on Sheaves and Logic, which will be held in the weekend of the 28th and 29th of June in Doorn, a place near Utrecht, the Netherlands. It is organized by the University of Utrecht with financial support from the MRI, the Mathematical Research Institute. We are glad to announce that this edition will feature a 3 hours tutorial by Clemens Berger on the subject of theta-categories, a topic from higher-dimensional category theory. The other confirmed speakers so far, are: Steve Awodey (Carnegie Mellon) Erik Palmgren (Uppsala University) Jonas Eliasson (Uppsala University) Christopher Mulvey (University of Sussex) The PSSL will take place at the conference centre "Kaap Doorn". The conference centre also offers rooms and meals, but only people who react before Friday the 6th of June are guaranteed to be offered this opportunity. FOR THIS REASON WE KINDLY URGE THOSE WHO ARE INTERESTED TO REGISTER BEFORE THE 6TH OF JUNE. (People who respond at a later date may have to stay at a hotel. In that case, special arrangements have to be made.) The all-in price for staying at the conference centre is 200-250 euro's. For further information and the latest list of participants, please consult the webpage (now fully operational): http://www.math.uu.nl/people/vdberg/PSSL79 People who wish to attend the PSSL should send an e-mail to vdberg(a)math.uu.nl indicating whether they you want to give a talk. Questions should be posted to the same address. With best regards, The organizers, Jaap van Oosten Federico de Marchi Pieter Hofstra Claire Kouwenhoven-Gentil Benno van den Berg -- Benno van den Berg - Mathematisch Instituut, UU vdberg(a)math.uu.nl - P.O.box 80.010, 3508 TA Utrecht, NL

1 0

Can we construct free semi-lattice from free dist. lattice?
by Christopher Townsend 28 May '03

28 May '03

Dear All, I have a problem which I had thought very specialised, but actually can be stated very generally: - I have a category C with finite limits, and so I also have a category DLat(C) of distributive lattices which, lets say, has coequalizers. If free distibrutive lattices can be constructed (i.e. if there exists F:C->DLat(C) left adjoint to the forgetful functor) then do free semilattices exist? Thanks, Christopher Townsend (OU)

2 1

Automata as Categories
by Steve Stevenson 22 May '03

22 May '03

I am interested to find an article or book that is a category- theoretic redevelopment of "classical" automata. I'd like to find something that graduate students could use if they had already had an automata course and now would retrace that same development using category-theoretic vocabulary and means. Thanks in advance... steve

5 4

localy compact spaces - computably based and over a topos
by Taylor Paul 21 May '03

21 May '03

Drafts of two new papers on Abstract Stone Duality are now available, and I would very much appreciate your comments about them. Computably based locally compact spaces An elementary theory of the category of locally compact locales http://www.di.unito.it/~pt/ASD These two papers bring ASD into line with the "official" theory of locally compact sober spaces and locales, in two completely different ways. The ASD "Manifesto" was also revised recently. =================================== Computably based locally compact spaces The first paper shows that the main version of ASD is equivalent to the category of "computably based" locally compact locales, and computably continuous functions. By a "basis" I mean a family of open subspaces U^n and accompanying family of compact subspaces K^n, the topological information being captured by the inclusion relation K^n subset U^m. For locales the corresponding idea is the "way below" relation. The finitary properties of this are characterised, including in particular the "Wilker condition" concerning the inclusion of a compact subspace in the union of two open ones. The motivation of the paper is principally how to "import" traditional topology into ASD, using the real line as a running example. This paper is the expanded version of the one that I presented at "Category Theory and Computer Science" in Ottawa and the "Domains Workshop" in Birmingham last August/September. =================================== An elementary theory of the category of locally compact locales The second paper shows that, when we add an "underlying set" axiom, the category becomes equivalent to the category of locally compact locales over any elementary topos. The usual structure of locale theory (direct and inverse image maps, Heyting implication, etc) is DERIVED, in a type-theoretic style. This is a new characterisation, not only of this category of spaces, but also of elementary toposes themselves. (The same technique can be applied to the opposite of the category of constructively completely distributive lattices, but I haven't filled in the details of this yet.) ASD axiomatises its category of spaces directly, not starting from a category of sets. However, the full subcategory of overt discrete spaces has emerged to fill this role. In the traditional situation, the forgetful functor from spaces to sets has both adjoints (the discrete and indiscriminate topologies), but of these three functors, only the leftmost exists in standard ASD. This paper postulates its right adjoint, which yields the couniversal overt discrete object related to any given space. (Such a thing would be unacceptable in the main theory, as the equality predicate on the underlying set of the powerset of N would solve the Halting Problem.) Whereas the category of sets is an (often unstated) assumption in a typical mathematical discourse, in this case the topos itself is constructed from the axioms, viz as this full subcategory. More significantly, the infinitary joins that are needed to axiomatise either traditional topology or locale theory are also a consequence of the axioms, and not a part of them. This is the sense in which the new axiomatisation deserves to be called elementary. In fact, the logical power of the theory (powersets in the topos, and the infinitary joins) arises out of the ``underlying set'' assumption. We have another example to show that closure of a full subcategory under (co)limits is a long way from providing an adjoint, and indeed the existence of the adjoint can be very strong foundational principle in itself. For example, when well-foundedness is presented in categorical terms using coalgebras, the extensional ones form a reflective subcategory, but the axiom of replacement may be needed to construct the reflection functor. See Exercise 9.62 in my book, "Practical Foundations of Mathematics". Paul Taylor pt(a)di.unito.it

1 0