Date: Fri, 27 Dec 1991 15:18 EST From: MTHFWL@ubvms.cc.buffalo.edu Lawvere and Schanuel's new book, CONCEPTUAL MATHEMATICS: A first Introduction to Categories (Preliminary version), 347+vii pp, paper is now available from Buffalo Workshop Press, P.O.Box l7l, Buffalo, N.Y. l4226, USA. Presupposing only high-school algebra, it is intended both as a text for a first course in both finite and continuous mathematics, emphasizing explicit treatment of concepts as opposed to elaborate computational algorithms, as well as a leisurely introduction to the categorical outlook for workers in other areas. The price of the volume is US$20 plus $3 shipping. Bill Lawvere e-mail: mthfwl@Ubvmsb.cc.Buffalo.edu ============================================================== Date: January 6, 1992 Appended to this is a file listing sites containing material which has been announced on the categories list as available by anonymous ftp. The file is available by ftp in [anonymous.categories] at macc2.mta.ca (138.73.1.2) and it would be happy to be expanded. It will be resent to the categories list occasionally. I would be glad for any suggestions re format and appropriate data for this file, but it is not intended to include a lengthy, article-by-article description. Bob Rosebrugh +++++++++++++++++++++++++++ This is FTP.SITES in [anonymous.categories] at macc2.mta.ca (138.73.1.2) The following sites have anonymous ftp directories with documents of interest to subscribers to the categories list: Machine Directory(ies) Comment ------- ------------- ------- boole.stanford.edu /pub papers by Casley, Crew (36.8.0.65) Pratt et al. maths.su.oz.au /sydcat papers by the Sydney (129.78.68.2) categories group; computational cat theory software, seminar notices etc. theory.doc.ic.ac.uk /theory papers by Abramsky, Taylor, (146.169.2.37) Vickers et al.; diagram macro package by Taylor triples.math.mcgill.ca /pub papers by Barr, Reyes, (132.206.150.30) Seely et al.; diagram macro package by Barr macc2.mta.ca [.mathcs.rosebrugh] papers by Rosebrugh and Wood (138.73.1.2) !note Vax syntax for cd as e.g. cd [.mathcs.rosebrugh] File updated 2 January 1992 ====================================== Subj: full sub-lex exponential ideals of lccc-s Date: Thu, 9 Jan 92 12:37:21 MET From: Thomas Streicher Does any body know the answer to the following question ? Is there a locally cartesian closed category C such that there is a full sub-left-exact category D of C which is non-reflective and forms an exponen- tial ideal, i.e. whenever A is an object in D and X is an object in C then [X->A] is (isomorphic to) an object in D ? The background to this question is the following. If something as described above would exist then one can perform the following construction. A morphism f : Y -> X in C is a DISPLAY MAP iff for any g : Z -> X : Pi (!Z) (g*f) : P -> 1 with P in D . For the collection DISP of display maps then one can prove : i) display maps are stable under arbitrary pullbacks ii) for any I in C : DISP / I ---> C / I reflects finite limits (iii) if f : X -> I is a display map and g : I -> J is an arbitary morphism in C then Pi (g) (f) is a display map as well . Now if D forms an exponential ideal then DISP / 1 is equivalent to D and we would get that the full subcategory of C (in the fibrational sense) is not reflective w.r.t. C / C . This would give an answer to a question I raised on this forum about one year ago. Thomas Streicher ====================================== Subj: Re: full sub-lex exponential ideals of lccc-s Date: Sat, 11 Jan 92 09:59:32 EST From: pjf@saul.cis.upenn.edu (Peter Freyd) The method I described to get examples for Streicher's request can, in fact, be easily modified to achieve full completeness. Let me give a specific example. Let D be the opposite of the ordered set of all ordinals. Except for the existence of a bottom element it is a Heyting algebra, therefore a local CCC. Let C be the result of adjoining a bottom element. Then D is a full left-closed exponential ideal in C. The bottom of C does not have a reflection in D. QEF Best thoughts peter freyd ====================================== Subj: Re: full sub-lex exponential ideals of lccc-s Date: Mon, 13 Jan 92 12:19:05 MET From: Thomas Streicher Thanks for the nice counterexample ! I think what you meant is that the constru- ction works for all Heyting algebras (I mean the finitary version : inf-semi-lat tice with exponentiation, no infinite sups or infs are claimed) without a least element. So the archetypical example is the natural numbers with an element for infinity together with the inverse ordering. By the way the display maps in a ll these examples are definable in the sense that whenever f : X -> I is an arbitrary map then there is a greatest subob- ject m : J >--> I such that m*f is a display map. Thus we have definability in the sense of Benabou. In all these cases either m is identity or J = 0 . May it be correct that there are only posetal counterexamples because in this case equalizers do not cause any problems ?? Thomas Streicher ====================================== Subj: Re: full sub-lex exponential ideals of lccc-s Date: Mon, 13 Jan 92 13:20:48 -0500 From: pjf@linc.cis.upenn.edu (Peter Freyd) [ the first of Peter's messages did not arrive the first time, and the moderator missed that reference in the second. Sorry about that. Bob Rosebrugh ] I sent two messages to the categories net only the second of which seems to have been distributed. The second begins by referring to the first. The following is a slightly edited version of the first message: ******************************************************************** I wonder if Thomas Streicher's question is really as he states it. Take any Heyting Algebra and "ideal", that is, a subset closed under finite meet and hereditary upwards. Then the ideal is a full "sub-left-exact" subcategory and it is an exponential ideal. The bottom element of the Heyting Algebra has a reflection in the ideal iff the ideal is principal. If one wants the subcategory to be closed under the formation of arbitrary limits (not just finite limits) then there are counterexamples but none that I know that can be so easily described. Best thoughts, peter freyd ====================================== Subject: Re: full sub-lex exponential ideals of lccc-s Date: Tue, 14 Jan 92 21:06+0000 From: Paul Taylor I must be suffering from schizophrenia, because I can't remember this counterexample. Perhaps you'd remind me? PS What was the simplifying lemma about display maps which you presented at a PSSL in Cambridge in 1987? ====================================== Subj: Re: full sub-lex exponential ideals of lccc-s Date: Tue, 14 Jan 92 05:58:55 EST From: pjf@saul.cis.upenn.edu (Peter Freyd) With regard to the Thomas Streicher's question: May it be correct that there are only posetal counterexamples because in this case equalizers do not cause any problems ?? There may well be a sense in which the answer is yes. But consider the following: let C with subcategory D be a counterexample. Let A be any local CCC. Then A x C with subcategory A x D is also a counterexample. ====================================== Subj: Re: full sub-lex exponential ideals of lccc-s Date: Wed, 15 Jan 92 12:05:22 MET From: Thomas Streicher Thanks again. Due to this observation by choosing for A the categories Set , omega-Set or PER-omega we get counterexamples which are very rich. IsnBt it the case that by taking the product of some lccc A with e.g. the nat ural numbers with inverse order one gets some aspect of "time" into realizabili ty models which destroy the existence of existential quantifiers. Maybe it is worthwhile to investigate connections with Martin-LoefBs work in mathematics of infinity where he considers sequences of models of type theory in order to explain infinite objects. Thomas Streicher P.S. I think a further interesting counterexample is obtained by taking for C the product of 0mega-Set with (N u {infinity})* and for D the full subcatego ry which is the cartesian product of PER-omega with (N u {infinity})*. ====================================== Subj: Five Postings Date: Fri, 17 Jan 1992 20:55:04 EST From: categories@mta.ca Due to a mailer failure, most of you did not receive any of the messages following. A new mailer is promised soon. Five postings are concatenated here in hopes of avoiding a recurrence of the problem. Bob ] 000000000000000000000000000 Date: Thu, 16 Jan 92 14:21:46 +11 From: kelly_m@maths.su.oz.au (Max Kelly) Subject" Kan Complexes Does anyone know whether it is the case that a simplicial set B is Kan whenever it has the property that, for each A (or for each n-simplex A), homotopy of maps A ---> B is an equivalence relation? Of course here the maps f, g : A ---> B are said to be homotopic iff they are the restrictions of a map A x I ---> B. Michael Barr, in a recent letter to me, said that this is a fact known to topologists; but I don't seem to be able to prove it. I don't see how the property would even allow one to fill in a 1-horn; there doesn't seem to be enough there to get any non-degenerate map on the 2-skeleton. Am I missing something? Max Kelly, 16 Jan. 1111111111111111111111111111 Date: Thu, 16 Jan 92 08:22:04 AST From: Paul Taylor Subject: Thomas Streicher's counterexample Somewhere the impression has come about that I gave a counterexample to a question posed by Thomas Streicher. I think I should make it clear that whatever this counterexample was, I didn't give it! 222222222222222222222222222 Date: Thu, 16 Jan 92 11:45:48 EST From: barr@triples.Math.McGill.CA (Michael Barr) Subject: A model for NWF sets? The covariant powerset functor has no set-based initial model, but it seems that the class of well-founded extensional trees is an initial model. (A tree is well-founded if every downward chain is finite and extensional if no node has two isomorphic branches.) This is well-known to be a model of set theory, Goedel's standard model, in fact. For each n define the nth truncation function, t |--> t|n by saying that t|0 is a bare root and and if t is derived by attaching {t_i} to a bare root then t|n is the extensional reflection (there is one; the obvious equivalence relation is Church-Rosser) of the tree gotten by attaching {t_i|n-1} to a bare root. Every tree is so derived, from well-foundedness. Now define a metric on the class of trees by saying that d(t,t') is 2 to the negative of the greatest n such that t|n = t'|n. In other words the distance is 2^-n if t|n = t|n, but t|n+1 /= t'|n+1. Then the Cauchy completion of this class obviously looks like NWF trees. Does anyone know enough about Aczel's work to tell me if this is a model of his axioms? BTW, this Cauchy completion is a terminal coalgebra for the functor. And it makes a difference whether you Cauchy complete and then take the extensional trees or do it the other way round. In other words, it is possible for the limit of a sequence of non-extensional trees to be extensional, but such trees are _not_ in the model. The decisive example is the NWF set defined by x = {x,{x}}, which is clearly the same as the one defined by x = {x}. (But I defy you to prove it by starting with the first one; it is immediate if you begin with the second.) Michael 333333333333333333333333333333333333 Date: Thu, 16 Jan 92 16:48:26 EST From: barr@triples.Math.McGill.CA (Michael Barr) Subject: Amalgamation property for Heyting algebras? Michael Makkai has shown that something called the Craig Interpolation lemma is equivalent to fact that in Heyting algebras a pushout of an injection is an injection. Now it is easy to show that a pushout of an injection with a quotient map is an injection, so the question is reduced to the amalgamation property. Anyone have an easy proof of that? Michael 444444444444444444444444444444444444 Date: Fri, 17 Jan 92 15:34:00 MET From: Thomas Streicher Subject: background to my question I think it might be interesting for some people to get explained the background of the question I posed on the e-mail forum and which has been ANSWERED by P. FREYD in a very pleasing and hepful way. Some time ago I was asking myself two questions. In the situation that one is given an lccc C and a class of display maps D respresenting a full internally complete category of C : 1) does this imply that display maps are closed under composition, i.e one has strong sums for this question the answer is no and described in my MSCS paper "Dependence and Independence Results for (Impredicative) Type Theories " 2) if one assumes that there is a generic morphism for D then by an internalization of FAFT one can prove that the full subcat as given by D is reflective in the fibrational sense, i.e. one has weak sums or existential quantification now the question was whether existential quantification is still guaranteed if one drops the assumption that there exists a generic morphism, i.e. the assumption of SMALLness the answer to this last question is NO and the counterexample - BASED on Peter FREYDs helpful lemma - is the following : take an lccc C together with a class of display maps D representing a full internally complete subcat of C ; let N* be the category which is the opposite of natural numbers extended with an object inf strictly greater than all natural numbers n ; now N* x C is an lccc , too, but now take as display maps those morphisms (x -> y , f ) : (x,A) -> (y,I) where f : A -> I is in D and x = inf iff y = inf ; let us call this new class of display maps DN ; then for the lccc N* x C with this new class DN of diplay maps it is the case that DN represents a full internally complete subcat of N* x C BUT it is NOT reflective !! Another question arising in this context is : How is the whole question related to sub-lccc-ness of the category represented by D ?? We call D REPRESENTING a FULL SUB-LCC of C iff for any object I of C the full subcat D / I of C / I is a full sub-lccc . What I have shown in my MSCS paper is that If D represent a full sub-lccc of C then D is closed under composition !! On the other hand if D represents a full internally complete subcat of C and D is closed under composition then D represents a full sub-lcc of C . What I also have shown in my MSCS paper is that If you take for C the category w-Set and for D those morphisms corresponding to families of extensional pers then D is NOT closed under composition, thus it does not represent a full sub-lccc ! This, of course, does not immediately imply that the category of extensional pers is not lccc . BUT my counterexample contains more. I have constructed a morphism f : Y -> X where Y and X are extensional pers and such that it holds that the domain of Pi (! X) f is not isomorphic to an extensional per . Thus extensional pers do not form a sub-lccc of w-Set ! Even more one can show that X is Sigma replete and f represents a family of Sigma replete pers. Let us call Y.x the family of pers corresponding to f . Of course, there is more to be shown than that for any x in X the Y.x is Sigma replete ! (Thanks to Wesley Phoa for pointing me to this problem !) But as Y.x is [Z.x -> Sigma] for a family Z.x of pers , one can realize UNIFORMLY IN x that Y_x is Sigma replete ! Thus w.r.t. the following aspects in Synthetic Domain Theory the situation is the same as in ordinary domain theory : The category of predomains is complete, but not lccc ! Thomas Streicher ====================================== Subj: Kan complexes Date: Sun, 19 Jan 92 09:04:58 EST From: barr@triples.Math.McGill.CA (Michael Barr) I have to admit not having ever seen a proof of what Max was asking about. Here is the way I see it in dimension 1. I assume that it is similar, but more complicated in higher dimensions. Consider the beginnings of a simplicial set and assume that homotopy, which I will denote ~ is an ER: d^0 ----> X_1 <---- X_0 ----> d^1 with the degeneracy s in the middle. The presence of the degeneracy forces the homotopy relation to be reflexive, by the way, although that is not what is involved here, but it is what is behind Max' question. The crucial thing is that any 1-cell is a homotopy between its two vertices. If x in X_1, then x is a homotopy between d^0(x) and d^1(x). Now let x^0, x^1 in X_1 satisfy d^0(x^0) = d^0(x^1), which is the only equation satisfied by that kind of 1-horn. Then we have d^0(x^0) ~ d^1(x^0), d^0(x^0) ~ d^1(x^0) and d^0(x^0) = d^0(x^1). If homotopy is to be an ER, we must have d^1(x^0) ~ d^1(x^1), which means that we need an element we will call x^2 in X_1 such that d^0(x^2) = d^1(x^0) and d^1(x^2) = d^1(x^1), which is the fill-in required. There are two other kinds of horns, depending on which simplex is omitted, but the one with x^1 omitted I have checked and it is similar and the third one is just the reverse of this one. This must be in some of the early papers of Kan (late 50s) or maybe John Moore (early 60s). Don't ask the categories net; ask algebraic topologists. Michael ====================================== Subj: representable 2-functors Date: Sun, 19 Jan 92 20:41:52 CST From: kapranov@math.nwu.edu (Mikhail Kapranov) I would like to be able to place a good reference about representable functors from a weak 2-category (or a bicategory,--this is what Benabou considered) to Cat -the 2-category of all categories. For example the correspondence that takes each object to the corresponding representable 2-functor is a (weak) equivalence of 2-categories (analog of Yoneda's lemma). This, in particular, shows at once that any WEAK 2-category is weakly 2-equivalent to a STRICT one (where associativity for composition of 1-morphisms and the units arer strict). I suppose these things are well known to people, but what would be a good reference? Mikhail Kapranov ====================================== Subj: Re: Amalgamation property for Heyting algebras? Date: Mon, 20 Jan 92 09:10:09 +0000 From: Andrew.Pitts@cl.cam.ac.uk >Michael Makkai has shown that something called the Craig Interpolation >lemma is equivalent to fact that in Heyting algebras a pushout of an >injection is an injection. To be precise I think Michael was claiming a new proof of the latter fact (the equivalence of CI to pushout stability is well known, to some). >Now it is easy to show that a pushout of an >injection with a quotient map is an injection, so the question is >reduced to the amalgamation property. Anyone have an easy proof of >that? For a constructive (and easy!) proof see my paper "Amalgamation and interpolation in the category of Heyting algebras", Jour Pure Appl. Algebra 29(1983)155--165. Andy Pitts ====================================== Subj: Re: representable 2-functors From: street@macadam.mpce.mq.edu.au (Ross Street) Date: Tue, 21 Jan 92 16:35:55 EST > > Date: Sun, 19 Jan 92 20:41:52 CST > From: kapranov@math.nwu.edu (Mikhail Kapranov) > > I would like to be able to place a good reference about representable > functors from a weak 2-category (or a bicategory,--this is what > Benabou considered) to Cat -the 2-category of all categories. > For example the correspondence that takes each object to the > corresponding representable 2-functor is a (weak) equivalence > of 2-categories (analog of Yoneda's lemma). This, in particular, > shows at once that any WEAK 2-category is weakly 2-equivalent > to a STRICT one (where associativity for composition > of 1-morphisms and the units arer strict). > I suppose these things are well known to people, but what would > be a good reference? > > Mikhail Kapranov > The Yoneda Lemma for bicategories appears in my paper "Fibrations in bicategories" Cahiers top et geom diff 21 (1980) 111-160 [A correction, not to do with the Yoneda Lemma, is in 28 (1987) 53-56.] The application of this result to coherence for bicategories was realised in the last year by Robert Gordon and John Power. It was discussed very openly at the Category Theory Conference in Montreal Mid 1991. I remember knowing of the application of the Yoneda Lemma to homomorphisms [essentially that every fibration is equivalent to a split one, as per Giraud's book] in the late 60's, but I do not recall observing, and know of no old reference for the Gordon-Power realisation. [For readers who missed out in Montreal, the point is that: given a bicategory K, there is a homom of bicategories K --> Hom(K^op,Cat) which is an equivalence on hom-categories; but Hom(K^op,Cat) is a 2-category; so K is biequivalent to the full sub-2-category of Hom(K^op,Cat) consisting of the representables. This gives a different proof of Mac Lane's coherence theorem for monoidal categories and of the Mac Lane-Pare version for bicategories.] A full account of a very slightly modified version of this approach to coherence of monoidal (=tensor) categories appears in Joyal-Street "Braided tensor categories" (still to appear in Advances in Math). We go on to do coherence for tensor functors (=strong monoidal functors) and braided tensor categories. Furthermore, Gordon, Power and I have used a similar technique to prove a coherence theorem for tricategories. This was announced in the Abstracts for the American Math Soc Meeting in Baltimore a week or so ago; Bob Gordon gave a talk at that conference. We have a paper in preparation. [Tricategories are like 3-categories except that composition of 1-cells is only associative up to equivalence and is only a homomorphism of bicategories &c &c.] While every bicategory is biequivalent to a 2-category, not every tricategory is triequivalent to a 3-category; the Gray tensor product is relevant, as expected after the work of Joyal-Tierney on homotopy 3-types. Regards to all, --Ross Street ====================================== Subj: Re: Amalgamation Property ... Date: Wed, 22 Jan 92 16:18:13 EST From: barr@triples.Math.McGill.CA (Michael Barr) I would still like to see a simple algebraic proof based on the fact that a cyclic H-module is flat, for a Heyting alg H. Andy's proof didn't seem all that easy to me. The background is that there is a notion of H-module and the pushout of a pair of Heyting algebra maps out of H is also the tensor product of H-modules. By an H-module I mean a sup semi-lattice that has unary ops x /\ - and x ==> - for each element x of H, and satisfying the obvious identities. Now for a ring R if every cyclic R-module is flat, so is every R-module. Here, every cyclic H-module is flat. Are they all? Michael ====================================== Subj: my recent question whether a complex is Kan if homotopy is an ER. Date: Fri, 24 Jan 92 14:10:25 +11 From: kelly_m@maths.su.oz.au (Max Kelly) Michael Barr's letter of 19 Jan to the bulletin board about this seems to me to be based on a misunderstanding. He says he shows how to fill in a 1-horn; but all he does is to produce the third side of a triangle when two sides are given - while what the Kan property demands is that one be able to fill in the whole triangle, interior and all. My difficulty was to see how to get any non- -trivial stuff on the interior at all, using "homotopy is an ER". At any rate, I have now received a counter-example from Bill Dwyer at Notre Dame; here it is: -------------------------------------------------- I'm beginning to think that the answer to your question is "no". Here's a possible counterexample and a line of argument. Suppose that E is the category with one object x and one non-identity morphism e: x-->x, where e^2=e. Then (1) If C is a category and F, G: C --> E are functors, then F and G are connected by a natural transformation. In fact, the function which assigns to any morphism of C the map e: x --> x is a natural transformation from F to G. There are only four diagrams to check: 1 1 e e x ---> x x ---> x x ---> x x ---> x e | | e e | | e e | | e e | | e V V V V V V V V x ---> x x ---> x x ---> x x ---> x 1 e 1 e (2) Let N be the nerve functor from categories to simplicial sets and L its left adjoint. L assigns to any simplicial set A the category whose objects are the vertices of A and whose morphisms are generated by the one-simplices of A, with one relation for each two-simplex. Let f, g: A --> N(E) be two simplicial maps. These correspond to functors F, G: L(A) --> E. As in (1) there is a natural transformation between F and G, which passes to a homotopy H : N(L(A)) x \Delta[1] ----> N(E) between N(F) and N(G). Composing H with the map A x \Delta[1] -----> N(L(A)) x \Delta [1] induced by the adjunction map A --> N(L(A)) gives a homotopy between f and g. In other words, for any two maps f, g: A --> N(E) there is a homotopy from f to g, so that in particular homotopy is an equivalence relation on maps A -> N(E). (3) N(E) is not a Kan complex. The nerve of a category is a Kan complex iff the category is a groupoid. For instance, in N(E) the following cofiguration cannot be extended to a two-simplex, because e does not have an inverse. x A e / / x ---> z 1 I think this is ok. Let me know if you find a hole in it. Bill Dwyer ---------------------------------------------------------- Max Kelly, 24 Jan. ====================================== Subject: 2-natural transformations Date: Fri, 24 Jan 92 15:12:26 +11 From: kelly_m@maths.su.oz.au (Max Kelly) Does the community have any reaction to the following observation, that we have made these last few days? Let A and B be 2-categories, and F,G : A ---> B be 2-functors. There is a notion of 2-natural transformation t : F ---> G; such a t is not only to be natural, in the usual sense, with respect to 1-cells, but to have the appropriate property with respect to 2-cells as well. Certainly mere natural- ity does not imply 2-naturality, as one sees on taking for A the free-living 2-cell. Yet it DOES imply 2-naturality if A admits tensor products with the arrow-category 2 (or dually cotensor products with 2). A consequence is that the forgetful functor, from the category of finitary 2-monads on a locally-finitely-presentable 2-category A to the category of finitary monads on the underling category of A, is a fully-faithful functor with both adjoints. In particular, a finitary monad on Cat or such-like has at most one enrichment (although usually none) to a 2-monad; and similarly for the more common case of enrichability over the closed category of groupoids. John Power and Max Kelly, at Sydney - 24 Jan. ====================================== Subj: with some trepidation Date: Thu, 23 Jan 92 14:03 GMT From: MAP010@vaxa.bangor.ac.uk (Philip Ehlers) %This is a LaTeX file which outlines a possible counterexample %to the conjecture which was on the mailing board at the %beginning of the week. I apologise for forgetting who %originally asked the question, and for the somewhat eccentric %style of the answer! \documentstyle{article} \title{A Counter Example} \date{23 January 1991} \begin{document} \maketitle The question was asked, on the category theory mailing board, as to whether this conjecture is true. \newtheorem{Kan}{Conjecture} \begin{Kan} Let $B$ be a simplicial complex. If homotopy is an equivalence relation on ${\em SS}(A,B)$ for all $A \in ob({\em SS})$, then $B$ is a Kan complex. \end{Kan} I think I have a counter example, and would appreciate it if anyone could spot the flaw(s) in the argument. \rule{0mm}{20mm} Let B be the simplicial set which is the complete directed graph on three vertices. Pictorially, this is the following:- \begin{picture}(200,150) \put(50,110){\circle*{5}} \put(150,110){\circle*{5}} \put(100,20){\circle*{5}} \put(55,112){\vector(1,0){90}} \put(145,108){\vector(-1,0){90}} \put(55,105){\vector(1,-2){40}} \put(90,25){\vector(-1,2){40}} \put(145,105){\vector(-1,-2){40}} \put(110,25){\vector(1,2){40}} \end{picture} This simplicial set is clearly not Kan. \rule{0mm}{10mm} There are nine simplicial set morphisms $I \longrightarrow B$ which we shall call $f_{jk}$ where this maps the non-degenerate element of $I_1$ to the edge from $j$ to $k$ (for $j = k$ this is just the degenerate edge at $j$). We shall denote the non-degenerate element of $I_1$ by $\iota$. \rule{0mm}{10mm} Now, consider any $f:A \longrightarrow B$ for any simplicial set $A$. Since all $n$-simplices in $B$ are degenerate for $n \geq 2$, we have that $f_n(a) = sf_{jk}$ where $s$ is some combination of degeneracy maps; note that if $j = k$, then $s = s_0^n$. Since simplicial morphisms commute with the face and degeneracy maps, this means that $f$ is completely determined by its effect on the $0$-simplices and $1$-simplices. \rule{0mm}{10mm} We require to show that the relation of homotopy is an equivalence relation on the hom-set $\underline{\em SSets}(A,B)$ for any $A$. Clearly it is reflexive, as there is a simplicial set morphism from $(A \times I)$ to $B$ which is dummy in the second variable. \rule{0mm}{10mm} If we now consider any two simplicial morphims $f,g:A \longrightarrow B$ and a homotopy $F:(A \times I) \longrightarrow B$ from $f$ to $g$, we construct a homotopy $G$ from $g$ to $f$ as follows:- \[G_0(a,0) = F_0(a,1) \;\;\; \mbox{and} \;\;\; G_0(a,1) = F_0(a,0) \;\;\; \mbox{for} \;\;\; a \in A_0\] \[ \mbox{If} \;\;\; F_1(a,\iota) = f_{jk}(\iota) \;\;\; \mbox{then} \;\; \; G_1(a,\iota) = f_{kj}(\iota) \;\;\; \mbox{for} \;\;\; a \in A_1 .\] Since these are all the elements of $B$, this determines $G$. Clearly \[ G(a,s_0^n1) = F(a,s_0^n0) = g(a) \;\;\; \forall a \in A_n \] \[ G(a,s_0^n0) = F(a,s_0^n1) = f(a) \;\;\; \forall a \in A_n \] \rule{0mm}{10mm} Lastly, assume we have two homotopies, $F$ from $f$ to $g$ and $G$ from $g$ to $h$. Then, we construct a homotopy $H$ from $f$ to $h$ as follows:- \[ H_0(a,0) = G_0(a,0) = h_0(a) \;\;\; \mbox{and} \;\;\; H_0(a,1) = F_0(a,1) = f_0(a) \;\;\; \mbox{for} \;\;\; a \in A_0 .\] If $F_1(a,\iota) = f_{jk}(\iota)$ and If $G_1(a,\iota) = f_{kl}(\iota)$ then $H_1(a,\iota) = f_{jl}(\iota)$ for $a \in A_1$. This is transitivity, and so the example is complete. \rule{0mm}{20mm} Comments, please! \rule{100mm}{0mm} ${\em Phil}$ \end{document} ====================================== Subj: Kan complexes (twice) Date: Sun, 26 Jan 92 12:38:47 EST From: barr@triples.Math.McGill.CA (Michael Barr) Kan complexes Max is right; I forgot what I was doing. Nevertheless, I learned long ago that a simplicial set is Kan iff the homotopy relation on maps to that set is an equivalence. I tried to prove it here with no references and I cannot, but I can certainly give a plausibility argument. I'm not sure I ever knew the whole proof. It must be in papers of Kan, in the late 50s. The plausibility argument is that if x^0 and x^1, say, are such that d^0x^0 = d^0x^1 and I want to find a 2-simplex of which x^0 and x^1 are d^0 and d^1, I begin by showing that x^0 ~ s^0d^0x^0 = s^0d^0x^1 ~ x^1. It follows that there is a simplex of which x^0 and x^1 are two of the faces. Then you have to find one of which it is the first two faces and I am not sure how to proceed. To see that x^0 ~ s^0d^0x^0, we calculate that d^0s^1x^0 = s^0d^0x^0, while d^1s^1x^0 = x^0. Dwyer's example seems to be that the nerve of a category isn't Kan. Yes, in fact about 1970, Boardman and Vogt showed that the nerve of a category always satisfies the "middle Kan" condition, meaning that it satisfies the condition for all missing indices except the first and last, but is not in general Kan. But it is not clear what is the point of including Dwyer's example. It is certainly not an example of a complex in which homotopy is an equivalence relation. Michael ++++++++++++++++++++++++++ Date: Sun, 26 Jan 92 14:53:29 EST From: barr@triples.Math.McGill.CA (Michael Barr) The example from Philip Ehlers is interesting and, although I haven't checked it, I presume it is correct. On the other hand, my last posting is also right (and his example fails it too). And I _do_ remember being told that a complex is Kan iff homotopy is an ER. So what gives? Well, way back when I studied algebraic topology, we were told that two k simplexes in a SS were homotopy if there was an n-simplex (n > k) of which they were faces. Then homotopy of simplexes is the ER generated by this. Now when you triangulate a square (that is, I x I) you get two triangles, so that, for example, two 1-simplexes are homotopic, by the reln that Ehlers used, if there are a pair of simplexes with a common edge of which these are faces of the one and the other. Of course, these generate the same ER, but they are not the same ER and it is possible for one, but not the other, to be an ER. Michael ====================================== Subject: groups in GROUPOIDS From: dyetter@math.ksu.edu (David Yetter) Date: Mon, 27 Jan 92 9:20:08 CST I'm wondering whether anyone (most likely by anyone I mean Ross Street, Andre Joyal or Ronnie Brown, but I thought I'd ask the net) knows a structure theorem for groups in GROUPOIDS. I've worked out that if G is the group of objects, H the group of connected components and A the (necessarily abelian) group of automorphisms of the identity object, then the group of arrows must by a semi-direct product of G x_H G with A, with source and target maps being projections, but I have not been able to show or find a counter-example to the conjecture that the map assigning identity maps to objects must be (\Delta, 0) and composition must be addition on the A components, and forgetting the common target/source in the other components. This seems to be something which should be known, so before putting more time in, I thought I'd ask. --David Yetter ====================================== Subj: Re: my recent question whether a complex is Kan if homotopy is an ER. Date: Tue, 28 Jan 92 13:30 GMT From: MAP010@vaxc.bangor.ac.uk I have to apologise, because my example is incorrect - firstly, the proof of symmetry is wrong, and secondly, the proof of transitivity is wrong, and neither can be rectified - There is a homotopy from any edge to its end point, and a homotopy from the start of any edge to the edge itself. This kills symmetry - and transitivity fails because there is no homotopy between edges if they cover all three vertices, yet if (say) we have an edge from 0 to 1 and an edge from 1 to 2, we have a homotopy from 01 to 1 and a homotopy from 1 to 12. So the whole example fails - fairly comprehensively! As a matter of interest, why was the question asked in the first place? - also, has anyone asked Prof. Kan? I'll check my counter-examples more carefully next time! - Phil Ehlers ====================================== Subj: extensional realizability refutes Scotts axiom Date: Tue, 28 Jan 92 14:35:00 MET From: Thomas Streicher EXTENSIONAL REALIZABILITY REFUTES SCOTT'S AXIOM It is well known that in the category of w-Sets there are several full small internally complete subcategories : - PER : interprets propositions - complete extensional pers , Sigma replete pers : candidates for effective domains ! Now the idea might be to use PER as propositions to speak about effective domains. Of course, this is possible ! BUT the logic is quite weak in the sense that the Proposition expressing Scott's Axiom is not realized !! PROOF : Let SIG denote the per corresponding to the r.e. subobject classifier . If Scott's Axiom (see e.g. M. Hyland in the Como Proc. or P. Taylor in the LICS'91 Proc. !) were realizable then there would exist a realizable morphism M : ((N -> SIG) -> SIG) -> N* ( N is the predomain of natural numbers and N* is N with bottom) such that for all F in (N -> SIG) -> SIG) : (a) M(F) = )bot) iff F()lambda ) x . )top)) = )bot) and (b) M(F) = n implies F()lambda) x < n . )top)) = )top) . As M is realizable it is monotonic we have that for all F in (N -> SIG) -> SIG) : M(F) less_or_equal M()lambda ) f . )top)) . Thus M applied to the least element gives )bot) and there exists a natural number n such that for all other F M(F) = n . But that would mean that for all F which are not least it holds that f(k) = )top) for all k < n implies F(f) = )top) . BUT THIS IS A CONTRADICTION : consider F := )lambda) f . f(n) ; this F is nontrivial and F()lambda) x < n . )top)) = )bot) . Thus such an M (Modulus of Continuity) cannot exist . END OF PROOF Of course, this proof can be performed for any reasonable axiomatization of SDT in an extensional type theory : If N is a proposition we can prove that all elements of N are equal ! Thus all propositions contain at most one element ! Thus we are again back at the effective tripos over w-Set , i.e. in some sense the topos-theoretic approach to SDT is the best we can expect. Actually to my opinion we do not need the full topos logic it is sufficient to consider triposes. I think the axiom of comprehension : A type , P predicate on A --------------------------------- { x : A | P(x) } type is not very nice to work with syntactically. At least I do not know a nice treatment by proof rules. By the way it is not a real restriction : from any tripos we can construct the associated topos. Thomas Streicher ====================================== Subj: RE: groups in GROUPOIDS Date: January 30,1992 From: MAS013@vaxa.bangor.ac.uk Here is a reply to Dave Yetter's query. The Magic words are "crossed modules". The basic reference is : R.Brown and C.B.Spencer, G-groupoids, crossed modules and the fundamental groupoid of a topological group, Proc.Konink. Ned. Akad. Weten. 79, 1976, 296-302. The results seem to have been known earlier. In fact if one thinks of a groupoid as being a generalisation of an equivalence relation, the proof of the equivalence of crossed modules and groups in groupoids is but a slight generalisation of the undergraduate proof that normal subgroups and congruences are equivalent ways of presenting the same information. Does this give the sort of structure theory required? Tim Porter. ++++++++++++++++++++++ From: street@macadam.mpce.mq.edu.au (Ross Street) Date: Wed, 29 Jan 92 10:37:42 EST Dear David, In a bit of a hurry, but saw your message. Groups in GPD are crossed modules a la Whitehead. Is this what you want? There are many references (eg the Mq Math Report on Braided monoidal categories --1986 version). Regards, Ross ++++++++++++++++++++++ Date: Wed, 29 Jan 92 16:11:08 EST From: beck@math.cornell.edu (Jonathan Beck 726 Univ Room 305) Stephen Chase tells me that the answer to the question, if he understands it correctly, is contained in J.-L. Loday, "Spaces with finitely many nontrivial homotopy groups", JPAA 24(l982), Lemma 2.2, p. l83 and is "a crossed module." Jon Beck +++++++++++++++++++++ From: Paul Taylor Date: Wed, 29 Jan 92 14:17:45 GMT Internal categories in the category of groupoids. David Yetter asked whether there is a structure theorem for "groups in GROUPOIDS". I interpret this question as "models of the finite-product theory of groups in the category (which has finite products) of groupoids and homomorphisms". I have a suspicion that David had something different in mind, such as "groupoids in groups", but shall consider the question as posed. Remember, incidentally, that the category of sets is a full subcategory (preserving all sorts of structure) of the category of groupoids. [The latter is, unlike groups, (locally?) cartesian closed as well.] Now internal *categories* in groupoids [and this easily specialises to groups] seem a natural generalisation of the quotienting of a preorder to give a poset, ie the "skeletalisation". We know that there's no natural way of just picking one object from each isomorphism class - so instead take the entire isomorphism class and consider it as a group, ie as a component of the groupoid of objects. Commutative squares with two sides isomorphisms provide the groupoid of morphisms. The construction is universal in a way which I shall leave to the reader to formulate. This idea has an application to polymorphism. Eugenio Moggi and Martin Hyland once proposed as a categorical interpretation of quantification over types simply taking the product indexed by the set of [names of] objects of the category. [We have in mind categories with a small number of isomorphism classes of objects - it's quite possible to have a cartesian closed category with exactly two (nonisomorphic) objects - we call it a model of the lambda calculus with eta and surjective pairing.] Unfortunately this idea is not invariant under categorical equivalence, and is therefore objectionable to the sensibilities of semantic categoricians such as myself. However the idea may be re-interpreted internally in the category of groupoids, and then becomes invariant, as Edmund Robinson observed. In fact something similar, though slightly more complicated, arises naturally in stable domain theory. The trace factorisation (see my unpublished 1988 paper, available by anonymous FTP from theory.doc.ic.ac.uk) expresses stable functors as spans and cartesian transformations as rigid comparisons between them, making the original 2-category an internal category in the category of domains and rigid comparisons. In the case of coherence spaces, the latter is equivalent to just the category of graphs and embeddings; this easily generalises to dI-domains. For (my) quantitative domains [see my paper in the Manchester Category Theory and Computer Science proceedings, LNCS 389, also FTP] it is the category of groupoids and homomorphisms. In both these cases, second order quantification in the standard domain way [which has been attributed to Girard, but was in my thesis before, and I didn't regard it as original, though I don't know to whom to attribute it - probably Plotkin] coincides with the Moggi-Hyland-Robinson interpretation. Paul Taylor ====================================== Subj: Re: extensional realizability refutes Scotts axiom Date: Thu, 30 Jan 92 20:49:50 EST From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic) Actually to my opinion we do not need the full topos logic it is sufficient to consider triposes. I think the axiom of comprehension : A type , P predicate on A --------------------------------- { x : A | P(x) } type is not very nice to work with syntactically. I appreciate Thomas Streicher's interesting observation about PERs but I don't see how does it lead him to this opinion about the comprehension. Comprehension is not a special property of PERs, nor are PERs its special model. Comprehension doesn't seem to play any role here. PERs are used as propositions/truth values when one uses them to model something like the Theory of Constructions. (Comprehension comes in, I suppose, only in a paper where I showed that Constructions can be given a familiar "set-theoretical" appearance, Springer LNCS #530.) I do not understand the point of comparing whether it is better to use Constructions (with or without comprehension) or the internal language of a topos. These things are at different levels. (Tripos is clearly weaker. For some purposes, however, I am sure that even first order logic will do.) Regards to all, Dusko Pavlovic P.S. Concerning the proof-theoretical difficulties with comprehension (if this is meant by "not very nice to work with") I can only say that these difficulties can not be a sufficient reason to dismiss a logical operation. Comprehension is certainly less difficult than the sum or the existential quantifier. ====================================== Subj: Re: extensional realizability refutes Scotts axiom Date: Fri, 31 Jan 1992 13:54:22 +0100 From: Thomas Streicher Here are some remarks on Duskos reaction on my comments about comprehension. What I meant was the following : comprehension is a means for TRANSFORMING PROPOSITIONS (i.e. objects in the fibre of some hyperdoctrine) to DATATYPES (i.e. objects in the base) in other words it allows to CONSIDER collections of proofs as types of objects. That is what I would call a mixing of levels of language : "data" are "real objects" WHEREAS "proofs" are "meta objects" . So one might be able to define functions which depend on proof objects but deliver say natural numbers. If I remember correctly exactly this is what Dusko wants to avoid by his theory of predicates. Thomas Streicher P.S. I - of course - do not mean that comprehension is "inconsistent" BUT I mean that it changes the notion of algorithm considerably and in an unintuitive way.