May 1990 - Categories - categories.org.au

None
by Michael Barr 30 May '90

30 May '90

(( A glitch in passing mailing list jobs resulted in an apparent failure to resend the following with less delay. R.R. )) The double parentheses are actually square brackets. Category Theory for Computing Science: Update Michael Barr and Charles Wells Our text, Category Theory for Computing Science, Prentice Hall, 1990 (ISBN 0-13-120486-6) has just been published. We intend to maintain the text in the sense that programmers maintain their programs, by keeping a list of known errors and also of additions to the text that we think might be useful. (The latter will probably come in spurts as we go to meetings and find out about wonderful new applications of category theory to computing science.) We will periodically announce new errata and addenda on the category theory bulletin board. The latest TeX version of the complete list is available by e-mail or p-mail from either author. The update consists of three parts: 1. A list of errors discovered so far. 2. Additional examples, problems and pointers to the literature. 3. Additions to the list of references, pp. 417ff. of the text. Page references refer to the text. Any further corrections or suggestions for additional text will be welcome. 1. Errors ((p. xv)) In the Chapter Dependency Chart, there should be a diagonal line from Chapter 5 to Chapter 7. ((p. 92)) In Proposition 4.3.12 and its proof, the letter C (not the script C) is used with two different meanings. This can be corrected by changing C to S in the first line of the proposition, third line (first occurrence only), fourth line (last occurrence only) and in the first line of the proof (second occurrence only). ((p. 96)) The reference to Seely should be ((1987)) (the entry in the list of references, p. 425, was incomplete and is updated in the list of references below.) ((p. 102)) ``The'' not ``the'' in line 7. ((p. 345)) Line 2 of the answer to exercise 12.a: the last letter should be ``B'', not ``b''. ((p. 365)) In the answer to problem 8, beta C:Hom(C,C) to F(C). ((p. 431)) The word ``relation'' should also be indexed on p. 21. 2. Additional text ((p. xiii)) (Second paragraph) Another collection of papers is ((Pitt, Rydeheard, Dybjer, Pitts and Poigne, 1989)). ((p. 17)) ((Additional example of category.)) Let alpha be a relation from a set A to a set B and beta a relation from B to C (see 1.3.4). The composite beta o alpha is the relation from A to C defined as follows: If x is in A and z is in C, (x,z) is in beta o alpha if and only if there is an element y in B for which (x,y) in alpha and (y,z) in beta. With this definition of composition, the category of sets and relations} has sets as objects and relations as arrows. ((p. 71)) ((New exercise)) Show that the category of sets and relations is equivalent, in fact isomorphic, to its own dual (see 2.6.7). Answer: Let Rel denote the category of sets and relations. For a relation alpha from A to B, that is, a subset of A x B, let alpha\op denote the subset {(b,a) | (a,b) in A x B} of B x A. Let F:Rel to Rel\op be the identity on objects and for a relation alpha:A to B, let F(alpha)=alpha\op. F(alpha) is a relation from B to A in Rel, hence a relation from F(A)=A to F(B)=B in Rel\op. It is easy to check that if beta:B\to C, then F(beta o alpha)= alpha op o beta\op in Rel, so (beta o alpha)\op=beta\op o alpha\op in Rel\op. This says F(beta o alpha)=F(beta) o F(alpha), so F preserves composition. The identity relation on A is Delta_A= {(a,a) | a in A}, so Delta=Delta\op and F preserves identities. Since for any relation alpha, (alpha\op)\op=alpha, we have F o F is the identity functor on Rel, so is its own inverse. Hence F is an isomorphism. By Exercise 1, it is therefore an equivalence of categories. ((p. 96)) The applications of 2-categories have mushroomed and include ((Hoare, Ji Feng and Martin, 1990)), ((Moggi, 1989)), and ((Power, 1989)) in addition to the papers already listed. ((p. 97)) Second paragraph of Section 4.5: In addition to generalizing the Cayley Theorem, the Yoneda Lemma also has as a special case the embedding of a poset into its down-closed subsets. Also: set-valued functors are studied further in Sections 11.2 and 14.4. ((p. 257)) Besides ((Coquand, 1988)), Moggi ((1989)) also uses the Grothendieck construction in modeling polymorphism. ((p. 287)) Just before the exercise: See also ((Ehrhard, 1989)). ((p. 318)) Add comment: We considered presheaves as actions in Section 3.2. They occur in other guises in the categorical and computer science literature, too. For example, a functor F:A to Set, where A is a set treated as a discrete category, is a ``bag'' of elements of A. If a in A, the set F(a) denotes the multiplicity to which a occurs in A. See ((Taylor, 1989)) for an application in computing science. ((p. 325)) Goguen ((1990)) has developed a sheaf semantics for object oriented programs. 3. Additional references T. Ehrhard, Dictoses. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989. J. Goguen, Semantics of concurrent interacting objects. Preprint, Programming Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD, England. C. A. R. Hoare, He Jifeng and C. Martin, Pre-adjunctions in order-enriched categories. Preprint, Programming Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD, England. E. Moggi, A category-theoretic account of program modules. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989. D. Pitt, D. Rydeheard, P. Dybjer, A. Pitts and A. Poigne, eds. Category theory and computer science. Lecture Notes in Computer Science 389, Springer Verlag, 1989. A. J. Power, An abstract formulation for rewrite systems. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989. R. Seely, Modelling computations: a 2-categorical framework. In Proceedings of the Conference on Logic in Computer Science, IEEE, 1987. ((Corrected reference)). P. Taylor, Quantitative domains, groupoids and linear logic. In Category theory and computer science, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poigne, editors. Lecture Notes in Computer Science 389, Springer Verlag, 1989.

1 0

None
by INHB000 27 May '90

27 May '90

Dear Bob: How do you feel about whole papers. Charles and I have a joint paper of which I attach the title and (most of) the introduction. Perhaps it is just as well to distribute this much and say that anyone who wants the whole paper, either by email or pmail should write to me. Regards, Mike =========================================== On the limitations of sketches Michael Barr and Charles Wells Introduction Sketches, as described for example in ?Barr and Wells, 1985?, can be used to describe many, but not all, kinds of mathematical structure. Recently Wells ?1990? has described an extension of the notion to allow more powerful constructors than those given by limits and colimits to be used to described structures. This raises the question of exactly what can be sketched with an ordinary sketch. A remarkable theorem of Makkai and Par\'e ?1990? (and discovered independently by Lair) says that a category is sketchable if and only if it is accessible. This means that for some cardinal $\kappa$ the category has colimits of all $\kappa$ filtered diagrams and that every object is a $\kappa$ filtered colimit of $\kappa$ presentable objects. An object $C$ of a category is $\kappa$ presentable if the functor $\Hom(C,-)$ preserves the colimits of $\kappa$ filtered diagrams. Since in practice one can usually decide quite easily if a category is accessible, this gives a usable criterion for sketchability, without, unfortunately, giving any idea how to sketch certain theories. Consider the category of categories with finite limits and functors that preserve them. We are not supposing canonical finite limits; the functors are merely required to take a finite limit diagram in the source to some finite limit diagram over the same base in the target. At first, it would seem that a theory to describe the set of all finite limit cones in a category would require a universal quantifier, and thus would not be sketchable. On the other hand, it is easy to see that the category of these categories with finite limits and functors that preserve them is $\aleph_0$ accessible and therefore from the theorem mentioned previously is sketchable. In this paper we actually exhibit a simple sketch for that category. A similar argument works for the category of categories with weak finite limits (a cone is a weak limit if every other cone has at least one arrow to it). We indicate the minor change needed in the argument for the case of weak terminal objects. On the other hand, the related category of categories with sublimits (a cone is a sublimit if every other cone has at most one arrow to it) is not accessible and hence not sketchable. In this case, a universal quantifier or some higher order construct is needed. We show that a universal quantifier suffices. Among other things this shows that there is a class of first order sketches that has more expressive power than that of ordinary sketches.

1 0

Dependent Products and Sums
by Charles.Wells＠prg.oxford.ac.uk 24 May '90

24 May '90

Here is a short note for the bulletin board: I agree with Mike Barr that "dependent function" and "dependent product" express exactly what is going on and should be the terminology used. It is a THEOREM that a dependent product is a kind of sum, generalizing the well known fact that in sets A\x B is a sum of A copies of B. A similar remark applies to dependent functions. However, the introduction of the names "dependent product" for dependent function and "dependent sum" for "dependent product" has expelled us permanently from Paradise. The confusion would be as bad as it has been for the notation for set inclusion, which was irretrievably messed up when in the sixties people started using the sideways horseshoe to mean "included in but not equal to" instead of merely "included in", which had been the standard meaning for fifty years. What about "indexed product" and "indexed sum"?

1 0

None
by INHB000 24 May '90

24 May '90

Vaughn Pratt has discovered something missing from the Atrianglepair and Vtrianglepair macros. Anyone who wants the corrections should write to me. There is no point in trying to send it to you since they would get screwed up in transit. I must say that the phrases ``dependent sum'' and ``dependent product'' really meant nothing to me and Larry Paulson's note on ``dependent product'' and ``dependent function'' was a revelation to me. So I would advocate going back to those old terms, for what my opinion is worth. Michael Barr inhb(a)mcgillb.bitnet inhb(a)musicb.mcgill.ca

1 0

more errors in TTT
by KOSLOWJ＠MACALSTR.BITNET 15 May '90

15 May '90

Dear Michael, Here are two other errors not listed so far (I don't know whether Jim Otto found them): On page 234, neither "Corollary 5 of Section 5.4" nor "Exercise (CANON)" exist. Well, the exercise is not listed on page 339, so I could not find it. Are you going to post Jim's list? (If it was distributed over the network, I didn't get a copy.) Also, if a TeX source exists for the book, you could distribute a second edition in that form, bypassing Springer. I ran into some strange problem when running your error list through LaTeX: all square brackets, left ones as well as right ones, had been replaced by question marks, even though the character check list was ok. After the appropriate modification it ran fine. Sincerely yours, J"urgen

1 0

More TTT Errors
by Dwight Spencer 15 May '90

15 May '90

I noted your indirect response via cat-net. Here are some more for your checking that I noticed since my first message: Errors in TTT Book - 1. Page 53, diagram (7): the vertical arrows should be pointing upward. 2. Page 54, lines 5-6 from the bottom: "... definition of universal arrow ..." - well, this definition does not appear explicitly in Section 1.5 as suggested. It certainly arises from Lemma 3 on page 28, but no hint is given there as to that lemma's translation into universal arrows. 3. Page 55, line 4: the typing of the psi-A weak universal arrow should be "A -> RWA." in order to be consistent with the discussion at that point. 4. Page 55, line 14: "The arrows Ry ..." should be "The arrows y ...". 5. Page 64: the diagram at the bottom should be labeled "(1)". - Dwight Spencer Dept. of Computer Science and Engineering Oregon Graduate Institute

1 0

None
by INHB000 15 May '90

15 May '90

Dear Bob: In addition to the new errata from Jim Otto that I got a copy of this morning, I also recd directly the following, that you may want to distribute to the net. I HAVE NOT CHECKED OUT EITHER ONE, although Charles says the two errors reported below are correct(ly identified as errors). The sales having fallen to nearly infinitesimal, it is unlikely that there will ever be a second edition to include these errata in. =============================================================== I noted your errata for Toposes, Triples, and Theories, and apparently the errors I detected below were not on your list: 1. Page 27, second line from bottom: "T:S -> T" should be t:S -> T. 2. Page 53, middle of page: using "." as the composition operator and "n" for eta, the derivation should be i(T,LA)(L(f.h)) = nA.f.h = RLf.nD.h = RLf.i(T,LD)(Lh) = i(T,LA)(Lf.Lh) . - Dwight Spencer Dept. of Computer Science and Engineering Oregon Graduate Institute =============================================================== Meantime, Category Theory for Computing Science ought to be out about now. Cheers, Mike

1 0

TTT errata
by unknown＠categories.mta.ca 14 May '90

14 May '90

Thanks for the TTT errata. I asked for it as TTT has been a big influence on me (for studying 1. initial le models of Horn theories, 2. free lcc's over generic objects). Additionally I have found: p 89: Refs Osius ?74, 75? are not in the bibliography (p 337). p 137: Thm 5 seems to lack enough hypotheses to apply prop 4 in its pf. Why is cat C^T exact? p 172: P having a left adjoint does not imply T does. (T = P o op(P). E(A, PP B) nat iso E(A x P B, P 1) nat iso E(P B, P A).) But T having a left adjoint is irrelevant to T being a triple. Also, a few months ago, a Penn grad student claimed to me, without details, that section 7.5 on Freyd's n.n.o. thm contains a subtle bug. Perhaps I will met you at lics in Phil. (1st week) or ctrs in Montreal (2nd week) this june (1st 2 weeks). Thanks Jim Otto ======================================================

1 0

None
by unknown＠categories.mta.ca 01 May '90

01 May '90

Additional errata (checked out): \item?p.27?, (Dwight Spencer) second line from bottom: T:S\to T should be $t:S\to T$. \item?p. 53? (Dwight Spencer) The display in the middle of the page should be: $i(T,LA)(L(f\o h)) = \eta A\o f\o h = RLf\o \eta D\o h = RLf\o i(T,LD)(Lh) = i(T,LA)(Lf\o Lh)$ In diagram (7), just below, the vertical arrows should be pointing upward. \item?p. 54? lines 5 from the bottom: (Dwight Spencer) change ``arrow for'' to ``element of the functor''. Add to the last sentence ``(A universal element of $\Hom(A,R(-))$ is called a {\bf universal arrow} for $R$ and $A$.)'' \item?p. 55? line 4: (Dwight Spencer) change $RLA$ to $RWA$. \item?p. 55? line 14: (Dwight Spencer) Change $Ry$ to $y$. \item ?p. 64? (Dwight Spencer) The diagram at the bottom should be labeled (1). (I don't think it is actually referred to, but the diagram numbering in this section begins with (2).) \item?p. 89} (Jim Otto) Refs Osius ?74, 75? are not in the bibliography (p 337). \item?p. 137? (Jim Otto) Theorem 5 has too few hypotheses and Proposition 4 too many to apply the latter in the proof of the former. There are various possibilities of getting it right, including adding the finite limits and colimits to the hypotheses of Theorem 5. But that theorem is true as it stands. Probably the best is to first point out first that only equalizers and coequalizers are needed and then only the $U$-contractible ones. Finally, if we suppose only the $U$-contractible coequalizers exist (any that exist will be preserved by a functor that has a right adjoint), that is enough to do Theorem 5 (Exercise, using the fact that the underlying functor of a tripleable functor creates limits) and from that will follow that the $U$-contractible equalizers exist. If we suppose that $\Bsc$ has $U$-contractible equalizers, the dual of Theorem 5 would imply that $U$-contractible equalizers exist. Hence sufficient for Proposition 5 is that {\em either\/} $U$-contractible equalizers or $U$-contractible coequalizers exist. Does anyone want to find an example to show that any completeness hypothesis is necessary? \item?p. 172? Second sentence: $\P$ having a left adjoint does not imply $T$ does. The sentence and following one should be combined as follows: ``Since $\T$ is the composite of a functor and its right adjoint, it is the functor part of a triple $(T,\eta:1\to T,\mu:T^2\to T)$.'' \item?p. 234? second paragraph (J\"urgen Kozlowski): Change Corollary 5 of Section 5.4 to Corollary 8 of Section 5.3. Also, Exercise CANON doesn't exist; delete the reference. \vskip1ex\noindent (Two missing references noted by J\"urgen Kozlowski): \vskip1ex\noindent G. Osius, Categorial set theory: a characterization of the category of sets. J. Pure Applied Algebra, {\bf 4} (1974), 79--119. \vskip1ex\noindent G. Osius, Logical and set theoretical tools in elementary topoi. Model Theory and Topoi, \lnm{445} (1975), 297--346.

1 0

commutative diagrams
by unknown＠categories.mta.ca 01 May '90

01 May '90

I am writing a book on equational logic and theorem proving for final year undergraduates, and want to include a formal treatment of commutative diagrams. Actually, I have never seen a formal treatment for pasting commutative diagrams, though I would be surprised if none existed. The following is my attempt to find an approach which is both elementary and sufficiently general for the usual applications. (A diagram is of course a consistent labelling of a graph by sets on nodes and functions on edges; set theoretically it is a function, so it makes sense to take unions and intersections of diagrams, although I admit this is excessively concrete.) \bdfn A ?\bf bipath? is a diagram $P$ with given nodes $s,t$ called its ?\bf source? and ?\bf target?, and given paths $p,q$ from $s$ to $t$, such that $P$ is the union of $p,q$ and $p,q$ intersect only at $s$ and $t$. \edfn \blemma Let $P_0$ and $P_1$ be commutative bipaths that intersect in just one path (possibly empty or one point). Then $P = P_0 \cup P_1$ is a commutative diagram. \elemma We can use this in proving the following more general result, by induction on the number of commutative bipaths which intersect $p$ and $q$: \bprop Given a collection $P_i$ for $i \in I$ of commutative bipaths such that each pair intersects in one path (possibly empty or one point), then any two paths $p,q$ in $P = \bigcup_?i \in I? P_i$ which start at the same source and end at the same target form a commutative bipath. \eprop Given the lemma, the proposition has a reasonably nice proof. Unfortunately, I have no way to prove the lemma except by an exhausting case analysis. Thus I would be grateful to hear about an alternative approach; a ``reduction'' to some advanced topic (such as 2-categories) would be interesting to me, but not actually useful for the purpose at hand. With many thanks, Joseph &&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&& Joseph A. Goguen, Professor of Computing Science, Programming Research Group, University of Oxford, 11 Keble Road, Oxford OX1 3QD, United Kingdom. email: goguen(a)prg.ox.ac.uk ?on the internet -- should also work in the U.K. on janet, but if not, try goguen(a)uk.ac.ox.prg -- Joseph.Goguen@... also works? phone: 272567 ?my office?; 272568 ?secy?; 273838 ?PRG office?; 272839 ?FAX? from USA, dial 011-44-865-...; from UK, dial (0865)-...

1 0