August 2001 - Categories - categories.org.au

paperback announcement: Categorical Logic and Type Theory
by Bart Jacobs 16 Mar '02

16 Mar '02

Dear Colleague, I am happy to announce that Elsevier has now published a paperback version of my book B. Jacobs, Categorical Logic and Type Theory Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999. 780 pages. The regular price of the paperback is NLG 150 / Euro 68.07 / US$ 74 Elsevier now offers a discount of 25% for this paperback if you order before 31 july 2001, using the attached form. In that case the price is: NLG 112.50 / Euro 51 / US$ 55.50. If you wish to use this special offer, please fill in the form, and send it in time to Andy Deelen at Elsevier (precise address at bottom of the form). Do not send it to me. The book gives a survey of categorical logic and type theory starting from the unifying concept of a fibration. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists. It contains the following chapters. Prospectus Introduction to fibred category theory Simple type theory Equational Logic First order predicate logic Higher order predicate logic The effective topos Internal category theory Polymorphic type theory Advanced fibred category theory First order dependent type theory Higher order dependent type theory References Notation index Subject index More information can be obtained from the authors webpage: http://www.cs.kun.nl/~bart/CLT/bookinfo.html Bart Jacobs, Dep. Comp. Sci., Univ. Nijmegen, P.O. Box 9010, 6500 GL Nijmegen, The Netherlands. Email: bart(a)cs.kun.nl PS. Please pass this information on to your institute's librarian.

2 1

the alpha of Omega
by Keith Harbaugh 07 Sep '01

07 Sep '01

While the topic of topos subobject classifier is current, how far back can the historical and conceptual origins of the use of "$\Omega$" as the symbol denoting such be traced? Regards, Keith Harbaugh 30-Aug-2001 07:15:05 -0300,1069;000000000000-0000001f

6 5

Comments on diagxy
by Michael Barr 01 Sep '01

01 Sep '01

\documentclass{article} \input mtex \input diagxy \input xymatrix \begin{document} When I created diagxy I did not set out to make diagrams that were better than those of xy-pic, but only to make a simpler and more familiar (to users of my diagram macros) interface. Since it is based entirely on xy-pic, it is not possible in any case. But then there are defaults\ldots. A colleague asked me to look at a paper to help him choose a referee and I came on the following display: $$\xymatrix { X_{rs}\ar[rr]^{\Upsilon_{(rs,\tau)}}&& X_{^\tau(rs)}\ar[rr]^{\Upsilon_{(^\tau(rs), \sigma)}}&&X_{^{\sigma\tau}(rs)} } $$ I don't know that the above code is the exact code the authors used, but the results are identical. I call your attention to the varying heights of the three $X$'s. For an extreme example of this, consider $$\bfig \xymatrix{X^\Gamma\ar[r]&x_\gamma} \efig$$ This happens because xymatrix centers the arrow on the middle of the node. I do not know if xymatrix can be told to do otherwise, but the underlying xy-pic code certainly can be and that was the default I chose in designing my morphism macro. Look at $$\bfig \morphism<900,0>[X_{rs}`X_{^\tau(rs)};{\Upsilon_{(rs,\tau)}}] \morphism(900,0)<900,0>[X_{^\tau(rs)}`X_{^{\sigma\tau}(rs)}; {\Upsilon_{(^\tau(rs),\sigma)}}] \efig$$ by contrast. The morphism code actually raises the arrow by a fixed amount (some fraction of the xheight, a font-dependent quantity) above the baseline, which is independent of descenders, ascenders, and sub- and superscripts. Actually, I would have done this with online to, which uses xy-pic only for the arrows, not the nodes and adjusts the lengths of the arrows to fit the labels: $$X_{rs}\to^{\Upsilon_{(rs,\tau)}}X_{^\tau(rs)}\to^{\Upsilon_{(^\tau(rs), \sigma)}}X_{^{\sigma\tau}(rs)}$$ This is not intended as a criticism of xy-pic. It is very general and it would be easy to find examples in which their default was what is wanted. It is just not likely to be in commutative diagrams. They do give the option of placing the arrow with respect to the baseline, which is more than Latex' picture mode does. My old macros were based on that. I now think it may be possible to coerce the picture mode into using the baseline (by putting things into boxes and defining them to have depth 0, if you want the details), but I knew much less 15 years ago when I started using Latex. So I used a different, much less satisfactory, approach that sort of worked but caused other problems and required extensive use of phantom arguments. \kern5pt\noindent Michael \end{document}

1 0

Workshop: History of Categories
by Robert A.G. Seely 01 Sep '01

01 Sep '01

------------------------------------------------------------------------------- HISTOIRE DE CATEGORIES 13 ET 14 SEPTEMBRE 2001 CENTRE DE RECHERCHES MATHEMATIQUES Universite de Montreal pavillon Andre-Aisenstadt, salle 4336 SPEAKERS : Liliane Beaulieu (CRM), Christian Houzel (CNRS -Paris 7), Jim Lambek (McGill), Mihail Makkai (McGill), Colin McLarty (Case Western Reserve), Gonzalo Reyes (U. de Montr�al). PROGRAMME 13 SEPTEMBRE 13h45 G. REYES, Topos theory in Montreal in the 70's: my personal involvement. 14h45 Discussion 15h00 Pause-cafe CRM 15h30 C. HOUZEL, Ehresmann sur les recollements dans la theorie des categories. 16h30 Discussion 17h00 The End 14 SEPTEMBRE 9h00 C. McLARTY, How the angel of topology and the devil of abstract algebra collaborated to make topology functorial. 10h00 Discussion 10h15 J. LAMBEK, Recollections of a reluctant categorist. 11h15 Discussion 11h30 M. MAKKAI, Categories in the foundations: a selective history. 12h30 Discussion 12h45 Lunch 14h15 L. BEAULIEU, Genese des notions de structure et (iso)morphisme chez N. Bourbaki. 15h15 Discussion 15h30 The End INFORMATION L. Beaulieu, CRM, beaulieu(a)crm.umontreal.ca L. Belair, UQAM, belair.luc(a)uqam.ca

1 0

Modules in a topos
by Michael Barr 30 Aug '01

30 Aug '01

What is a good source for the category of modules over a ring object in a Grothendieck topos? I am particularly interested in the question: if I is an injective module and E is an object of the topos, then there is an exponential I^E. Is it injective? Equivalently, are internal copowers left exact? Michael 30-Aug-2001 10:34:31 -0300,1968;000000000000-00000020

1 0

book: Infinite Homotopy Theory
by Elizabeth Douglas 27 Aug '01

27 Aug '01

Kluwer Academic Publishers are pleased to announce the launch of Infinite Homotopy Theory edited by H-J Baues and A. Quintero. Infinite Homotopy Theory provides an up to date, comprehensive coverage of the area and deals with algebraic topology, homotopy thoery and simple homotopy theory of infinite CW-complexes with ends. More information can be found at http://www.wkap.nl/book.htm/0-7923-6982-3 Liz Douglas Product Manager Tel +31 (0)78 6392 204 Fax: +31(0)78 6392 323 e mail: elizabeth.douglas(a)wkap.nl http://www.wkap.nl 30-Aug-2001 07:11:39 -0300,925;000000000000-0000001e

1 0

TACS2001 PROGRAM AND REGISTRATION INFORMATION
by Shinya MIYAKAWA 27 Aug '01

27 Aug '01

<<Apologies if you receive multiple copies.>> PROGRAM AND REGISTRATION INFORMATION International Symposium on Theoretical Aspects of Computer Software (TACS2001) Tohoku University, Sendai, Japan October 28-31, 2001 Further information about TACS2001 can be obtained on the Web, at: http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ Any inquiry on TACS2001 Program and Registration may be directed to TACS2001(a)ito.ecei.tohoku.ac.jp ====================================================================== TACS2001 PROGRAM ^^^^^^^^^^^^^^^^ OCTOBER 28 SUNDAY 16:00 REGISTRATION at Sendai Tokyu Hotel till 21:00 19:30 WELCOME RECEPTION at Sendai Tokyu Hotel till 21:00 OCTOBER 29 MONDAY at Aoba Memorial Building, Tohoku University INVITED TALK 1 9:10 A Spatial Logic for Concurrency Luca Cardelli (joint work with Luis Caires) 10:10 Break SESSION 1, 10:30 - 12:00 10:30 Boxed Ambients Michele Bugliesi, Giuseppe Castagna, Silvia Crafa 11:00 A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation Daisuke Hoshina, Eijiro Sumii and Akinori Yonezawa 11:30 Formal Eavesdropping and its Computational Interpretation Martin Abadi and Jan Jurjens 12:00 Lunch Break INVITED TALK 2 13:15 Resource-Passing Concurrent Programming Kazunori Ueda 14:15 Break SESSION 2, 14:35 - 15:35 14:35 Solo Diagrams Cosimo Laneve, Joachim Parrow, Bjorn Victor 15:05 Observational Equivalence for Synchronized Graph Rewriting with Mobility Barbara Koenig and Ugo Montanari 15:35 Break SESSION 3, 15:55 - 17:25 15:55 Fixed-point Logic with the Approximation Modality and its Kripke Completeness Hiroshi Nakano 16:25 Termination Proofs and Complexity Certification Daniel Leivant 16:55 A Renee Equation for Algorithmic Complexity Keye Martin 17:25 Break OCTOBER 30 TUESDAY at Aoba Memorial Building, Tohoku University INVITED TALK 3 9:10 Nominal Logic: A First Order Theory of Names and Binding Andrew M. Pitts 10:10 Break SESSION 4, 10:30 - 12:00 10:30 A Logic Programming Language based on Binding Algebras Makoto Hamana 11:00 Proof-search and Countermodel Generation in Propositional BI Logic Didier Galmiche and Daniel Mery 11:30 Generation of a Linear Time Query Processing Algorithm based on Well-Quasi-Orders Mizuhito Ogawa 12:00 Lunch Break INVITED TALK 4 13:15 Modelisation of Timed Automata in Coq Christine Paulin-Mohring 14:15 Break SESSION 5, 14:35 - 16:05 14:35 Model-Checking LTL with Regular Valuations for Pushdown Systems Javier Esparza, Antonin Kucera, Stefan Schwoon 15:05 What Will be Eventually True of Polynomial Hybrid Automata? Martin Fraenzle 15:35 Non-Structural Subtype Entailment in Automata Theory Joachim Niehren and Tim Priesnitz 16:05 Break SESSION 6, 16:25 - 17:25 16:25 Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems Ph. Schnoebelen 16:55 Weakest Congruence Results Concerning "Any-Lock" Antti Puhakka 17:25 Break 18:30 BANQUET at Sendai Tokyu Hotel till 20:30 OCTOBER 31st WEDNESDAY at Aoba Memorial Building, Tohoku University INVITED TALK 5 9:10 Design and Correctness of Program Transformations based on Control-Flow Analysis Jon G. Riecke (joint work with Anindya Banerjee and Nevin Heintze) 10:10 Break SESSION 7, 10:30 - 12:00 10:30 Infinite Intersection and Union Types for the Lazy Lambda Calculus Marcello M. Bonsangue and Joost N. Kok 11:00 Strong Normalization of Second Order Symmetric Lambda-mu Calculus Yoriyuki Yamagata 11:30 The Girard-Reynolds Isomorphism Philip Wadler 12:00 Lunch Break INVITED TALK 6 13:15 Lightweight Analysis of Object Interactions Daniel Jackson (joint work with Alan Fekete) 14:15 Break SESSION 8, 14:30 - 15:30 14:30 Typing Assembly Programs with Explicit Forwarding Lennart Beringer 15:00 The UDP Calculus: Rigorous Semantics for Real Networking Andrei Serjantov, Peter Sewell, Keith Wansbrough 15:30 Break OPEN LECTURE 15:45 Unison: A File Synchronizer and its Specification Benjamin C. Pierce (Joint work with Jerome Vouillon) 17:00 CLOSING SESSION till 17:10 -------------------------- 18:30 Japanese Dinner Party for Participants from Abroad ============================================================================== TACS2001 is sponsored by Tohoku University, Sendai, Japan in cooperation with Information Processing Society of Japan Japan Society for Software Science and Technology Association for Symbolic Logic Association for Computing Machinery--SIGACT Symposium Chair: Takayasu Ito Tohoku University Program Chairs: Naoki Kobayashi Tokyo Institute of Technology Benjamin Pierce University of Pennsylvania Program Committee Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann University of Edinburgh Zhenjiang Hu University of Tokyo Naoki Kobayashi Tokyo Institute of Technology Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark University of Edinburgh Makoto Tatuta National Institute of Informatics, Tokyo ========================================================================= GENERAL INFORMATION TACS2001 will be held on the campus of Tohoku University, Sendai, Japan. The invited talks and contributed talks will be presented at the Aoba Memorial Building, Faculty of Engineering located on the Aoba Hill about 3 km west of downtown Sendai. The welcome reception and banquet will be held at Sendai Tokyu Hotel, located in downtown Sendai. The TACS2001 proceedings will be available as a volume of Lecture Notes in Computer Science, Springer-Verlag, at the time of the conference. Sendai is the largest city in the northern part of Honshu Island of Japan, with a population of about a million. The city is known in Japan as the "City of Trees". It is 350 km north of Tokyo and about 2 hours away by the Tohoku Bullet Train (Tohoku Shinkansen). Sendai is a modern, safe city with a moderate climate blessed by four distinct seansons. At the end of October the weather would be mostly sunny with temperature ranging from 5 C (41 F) to 15 C (59 F), and it will be the time of beautiful autumnal tints. Conference registration is open to the public. Reservations for the Japanese dinner party (October 31st) will be limited. Register and make reservations by returning the completed form by email and fax. The registration form is attached below, and it is also available from the TACS2001 web site. There will also be on-site registration at: * Sendai Tokyu Hotel, 16:00 - 21:00, October 28, * Aoba Memorial Bldg, Tohoku Univ, 9:00 - 17:00 on October 29-31. Some information on transportation and hotels is described below. More information on TACS2001, including travel information, is available at the TACS2001 web page: http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ Transportation ^^^^^^^^^^^^^^ Conference participants arriving at the new Tokyo International (Narita) Airport are advised to take the JR Narita Express train from Narita Airport to Tokyo Station. Then take the Yamabiko super express train of Tohoku Shinkansen (Tohoku Bullet Train) from Tokyo to Sendai. Making reservation at Narita Station for the Yamabiko is strongly recommended. Those arriving at the new Osaka International (Kansai) Airport can fly to Sendai Airport, and take Limousine Bus service to Sendai Station. Alternatively, you can take a local train from the Kansai Airport to JR Shin Osaka Station, then take the Tokaido Shinkansen from JR Shin Osaka Station to JR Tokyo Station and change at Tokyo Station to Tohoku Shinkansen. Some details on transportation will be available at the TACS2001 web page. Note: (1) No flight service is available from Narita to Sendai Airport, since the train service is superior. There is another train service from Narita Airport to downtown Tokyo (Ueno) by Skyliner of the Keisei-Narita Line. At Ueno you can take the Yamabiko superexpress of Tohoku Shinkansen to Sendai, but you have to walk about 10 min from Keisei Ueno Station to JR Ueno Station to take Tohoku Shinkansen. (2) If you are going to travel in Japan by JR lines before/after the TACS2001 symposium, it will be convenient and economical to get a JR PASS before your departure. Contact your travel agent for more information on JR PASS (Japan Rail Pass). Hotels ^^^^^^ Two hotels offer discount rates to TACS2001 participants: the Sendai Tokyu Hotel, and the Sendai Washington Hotel. They are 1.2 km west of Sendai Station and about 800 Yen by taxi from the station. Two hotels are located within 5 min walk of each other. More information on TACS2001 is available at the TACS2001 web page. =========================================================================== REGISTRATION AND RESERVATION Registration Fees ^^^^^^^^^^^^^^^^^ Registration fees cover attendance in all sessions, a copy of proceedings, refreshments and snack, the welcome reception and banquet, but not the Japanese dinner party on October 31st. The reduced author rate applies to all authors of the accepted papers, and the reduced committee member rate applies to all members of the Program Committee and the Organizing Committee. The student rate applies to full time students. Registrants paying reduced rates have full privileges at the conference. The companion rate covers the welcome reception and banquet only. Through September 17 From September 18 Regular 40,000 Yen 50,000 Yen Author 30,000 Yen 40,000 Yen Committee Member 30,000 Yen 40,000 Yen Student 20,000 Yen 30,000 Yen Companion 4,000 Yen 6,000 Yen Hotels ^^^^^^ Two convenient Western style hotels offer TACS2001 discount rates. Rates are per person, per night, and include service charge and tax (not including breakfast). Single Room Twin Room Sendai Tokyu Hotel 10,185 Yen 7,560 Yen Sendai Washington Hotel II 8,000 Yen 7,000 Yen Sendai Washington Hotel I 7,000 Yen --------- Note: Twin room reservations are available for two persons. No roommate matching service is available, so twin room reservations remain registrant's responsibility. Japanese dinner party for participants from abroad ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ A Japanese dinner party for participants from abroad will be held at TOYOKAN in the evening of October 31st. The invited speakers, PC members, and some others will attend. A limited number of reservations will be available for this dinner party. The rates are as follows. Conference registrant: 10,000 Yen Companion: 6,000 Yen =================================================================================== Cut here to send your registration and reservation form after filling in the items. =================================================================================== TACS2001 REGISTRATION AND RESERVATION FORM Please register and make reservations by completing the form below and returning it by email to tcs02(a)thk.jtb.co.jp Registrants are advised to email a copy of their completed form to TACS2001(a)ito.ecei.tohoku.ac.jp They are also encouraged to send a signed, printed copy of their completed form by FAX to 022-296-3327 (domestic) +81-22-296-3327 (from abroad) which is the fax number of the following agent to take care of the conference registration and reservation. Japan Travel Bureau Group Tours Office Tohoku Tobu Sendai Daiichi Bldg, 6th Floor 4-6-1 Tsutsujigaoka, Miyagino-ku, Sendai 983-0852, Japan FAX: 022-296-3327 (domestic) +81-22-296-3327 (from abroad) PHONE: 022-296-3361 (domestic) +81-22-296-3361 (from abroad) Email: tcs02(a)thk.jtb.co.jp Registration and reservations will be completed by your payment, whose method is described below. "IMPORTANT NOTE" As described below, from the standpoint of the safety, registrants are advised to pay fees by Bank Transfer. When the payment is made by a credit card, they are advised to send the required information, including Credit Card numbers by FAX; that is, do NOT send Credit Card numbers by email. REGISTRATION FOR TACS2001 ^^^^^^^^^^^^^^^^^^^^^^^^^ Last (Family) Name: First (Given) Name: Middle: Affiliation: Postal Address: City/State/Zip: Country: Phone: Fax: Email: Registration Status <Regular, Author, Committee Member, Student>: Number of Companions: Companions' names (if applicable): (A) Total Registration Fee(s) in Yen: HOTEL RESERVATION ^^^^^^^^^^^^^^^^^ Hotel First Choice: Hotel Second Choice: Number of Single Room(s): Number of Twin Room(s): Roommate's Name(s) for Twin Room(s): Check-in Date: Check-out Date: Number of Nights: Special Room or other Request: JAPANESE DINNER PARTY ^^^^^^^^^^^^^^^^^^^^^ A limited number of reservations are available for the Japanese dinner party to be held at TOYOKAN in the evening of October 31st, for participants from abroad. (B) 10,000 Yen x [ ] conference registrant(s): (C) 6,000 Yen x [ ] companion(s): TOTAL FEE IN YEN ^^^^^^^^^^^^^^^^ (A) + (B) + (C): Signature (not needed for email): METHOD OF PAYMENT FOR TACS2001 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ From the standpoint of the safety and security, participants are encouraged to pay via Bank Transfer. When they pay via credit card, they are advised to send the required information (in particular, Credit Card numbers) by FAX; that is, do NOT send your Credit Card numbers by email. In credit card payment Visa card, MasterCard, and Diners card will be accepted. Personal checks cannot be accepted. All payments must be made in Japanese Yen. Indicate method of payment below: [ ] Bank Transfer to Bank: Tokyo Mitsubishi Bank, Sendai Branch Account Name: TACS2001 Chair Takayasu Ito Account No. 1180724 From <bank name>: Date of transfer: Payer's name: Note: In Japan the bank number of Tokyo Mitsubishi Bank is 0005, and the number of its Sendai Branch is 320. [ ] Payment by Credit Card Credit Card Type <Visa, MasterCard, or Diners>: Card Number: Expiration Date: Signature (not needed for email): <Note>: When your payment is via Credit Card, send the above information by FAX to +81-22-296-3327, the fax no. of Japan Travel Bureau Group Tours Office Tohoku. Even when you send the above form by fax, send it by EMAIL without filling in Credit Card number for safety. ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Registration and reservations will be confirmed upon receipt of payment. Refunds will be made upon written request received through October 15, 2001 by Japan Travel Bureau Group Tours Office Tohoku. -----*****-----*****-----*****----- 30-Aug-2001 07:11:27 -0300,1266;000000000000-0000001d

1 0

sum of pointed sets.
by peter_easthope＠gulfnet.sd64.bc.ca 25 Aug '01

25 Aug '01

Hypothesis: the sum of an m-pointed set and an n-pointed set is an m+n-pointed set. Is this true? I've not thought of a counterexample. If this is a theorem, can anyone tell me where to find a proof. Such a proof, presented by a professional mathematician, would be interesting and instructive. Thanks, peter_easthope(a)gulfnet.sd64.bc.ca 21-Aug-2001 10:16:08 -0300,1831;000000000000-00000014

2 1

Clarifying the classifier
by F. William Lawvere 25 Aug '01

25 Aug '01

To supplement Vaughn Pratt's excellent account of the subobject classifier in the topos of directed graphs, it may help to make explicit the following: The truth object merely represents (i.e., concentrates) a notion which applies in any category. Given two maps x and y with the same codomain, x BELONGS TO y iff the Steenrod lifting problem has a solution (Exist z) x=yz. If y is monic, then of course there is at most one "proof" z of such a belonging relation. Further specializing, if x is also monic, the relation in question is usually called "inclusion of parts" ; specializing in another direction, if the domain of x is a favorite element-kind in the particular category (such as a generic arrow or generic dot in the case of graphs, or the terminal object 1), then it is called "membership". Note that pioneers such as Dedekind and Banach did NOT need to distinguish notationally between these special cases (in contrast to the Peano tradition which seems to have brought more confusion than clarification). The dual Steenrod division problem, which he called "extension", is equally important in mathematical practice; existentially quantifying it we obtain a "delta" relation dual to the epsilon relation: f IS DETERMINED BY g iff there exists (a procedure) p so that f=pg. Again if g is epic there can be at most one p, and of interest is the case where the codomain of f is restricted to a favorite "type"(=space of values for functions). Question: Are there useful categories wherein this determination relation is concentrated in one object as the belonging relation is for toposes? >From: Vaughan Pratt <pratt(a)cs.stanford.edu> >To: categories(a)mta.ca >Subject: categories: Re: Subclassifier object question >Date: Mon, 20 Aug 2001 13:01:52 -0700 > >The direct answer to Bill Halchin's concern (`it seems like every >element will be "classified" as belonging to "subX"') is that this is >the defining characteristic of subX: subX consists of those elements >of X that belong to subX. That is, every element of subX has to be >classified as belonging to subX. > >The triviality of this answer suggests that Bill's real question is, >how does the pullback > > f > Y ----> X > | | > !| |g > | | > v z v > 1 ----> Z > >in the definition of topos work in the case of sets? Here's one answer. > >The basic idea is that there are two equally good ways of defining a >subset of a set X, in terms of functions respectively to and from X. > >TO: A function f:Y->X has an image f(Y), a subset of X. > >FROM: A function g:X->Z has an inverse image g^-1({z}) of any given >element z of Z, also a subset of X. > >Every subset of X arises in both ways (provided in the latter case that Z >has at least two elements). With a little care it can be made to arise >in a canonical way in both cases, and moreover such that these two ways >are paired up according to the subset they each determine. > >TO: Now there are many functions to X with the same image. However any >two _injections_ i:Y->X, i':Y'->X have the same image if and only if >there is a bijection j:Y->Y' for which the evident triangle commutes, >namely i'j = i. Call two such injections isomorphic. The isomorphism >classes of injections to X are then in bijection with the subsets of X. > >FROM: Even if we hold Z and an element z thereof fixed there may >still be many functions g:X->Z with the same inverse image g^-1({z}). >This happens for |Z| >= 3, where two g's can agree on the members of >a subset yet disagree about which of the non-z elements of Z to send >the nonmembers to. On the other side, if Z is a singleton we lose the >proper subsets of X, and if Z is empty we lose all subsets. > >We are now in a position to analyze the subobject classifier condition, >which can be stated for sets as follows. > > For every injection i:Y->X there exists a unique g:X->Z making the > above square a pullback. > >Existence and uniqueness each appear twice in this condition, once >explicitly, and once implicitly in the notion of pullback. > >For the former, the existence requirement ensures that Z has enough >elements to permit it to classify at all, while uniqueness prevents it >from having too many, avoiding ``overclassification.'' Thus |Z|=2 is >the only possible choice for a subobject classifier, i.e. Z (along with >its element z) is determined up to isomorphism. > >For the latter, the uniqueness requirement in the definition of pullback >ensures that i is an injection, and existence makes it the the maximal >injection into X for which g(i(y)) = z for all y in Y. Note furthermore >that g uniquely determines i up to isomorphism, i.e. the property of >being a pullback ensures that for each g there exists a unique i up to >isomorphism, giving us the other direction of our desired bijection. > >Although everything said above has been for Set, it can be lifted (with >the necessary care) to any cartesian closed category with the obvious >generalizations of set to object, function to morphism, injection to >monic, and element to morphism-from-1. > >What does not lift are properties of the topos Set not common to all >toposes, such as that Set has a natural numbers object {0,1,2,...}, >and is a Boolean topos (the logic of set membership is Boolean). > >An example of a topos with no natural numbers object is furnished by >the subtopos of Set consisting just of its finite sets. The argument >that Set is a topos shows with almost no modification (and in particular >with the same subobject classifier) that this evidently cartesian closed >subcategory is itself a topos. > >An example of a non-Boolean topos is furnished by the cartesian closed >category of directed graphs made a topos by taking Z to be the 2-clique >(two vertices and four edges) with one of its self-loops duplicated >and the duplicate taken as z (the elements of a directed graph being >its self-loops). A CCC can be made a topos in at most one way up to >isomorphism of its subobject classifier, so (given that this choice >works), this strange graph is it for this topos. > >One quick way to see that this is a topos is to present it as the >presheaf category Set^C where C is the category E=>V with two objects >E,V and two morphisms s,t:E->V. A graph is a functor from C to Set; >it assigns sets to E and V (respectively the set of edges and the set of >vertices), and functions to s and t, respectively the source and target >functions specifying the two vertices the edges run between. The relevant >theorem here is that the functor category Set^C is a topos for any small >category C. For C = E=>V the theorem automatically constructs the above >strange graph. > >Vaughan Pratt > 27-Aug-2001 07:06:29 -0300,2121;000000000001-0000001b

1 0

"catamorphism"
by Frank Atanassow 25 Aug '01

25 Aug '01

What is the definition/scope of the term "catamorphism"? In the calculational school of programming, I think people agree that: For every F-algebra A, the unique F-homomorphism from an initial F-algebra to A is a catamorphism. but: Is the converse true also, or is `catamorphism' more general: "a catamorphism is the unique arrow from an initial _object_ (in any category, not just categories of algebras)." I think the answer to that question is no, but is there a snappy name for such arrows? What about the universal arrows in the free algebra construction? Are those `catamorphisms' or not? If not, is there a name for those arrows? and furthermore: In the case of initial F-algebras, for F an endofunctor on category C, is the catamorphism the arrow in the category of F-algebras, or the corresponding one in C? In other words, is `catamorphism' a property of the arrow or the arrow + the category? If you compare with `monomorphism', since we speak of being `monic _in_ C', I presume the latter, and thus only one arrow would be `catamorphic', but which? Judging from the literature, I am inclined to say that the arrow in C is the catamorphism, but I would like a second opinion. -- Frank Atanassow, Information & Computing Sciences, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-3261 Fax +31 (030) 251-379 24-Aug-2001 12:14:45 -0300,2712;000000000000-00000018

2 1