Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
at foundation of mathematics I have tried to start an Idea-section.
Also, I am hereby moving a bunch of old discussion boxes from there to here:
[ begin forwarded discussion ]
+– {: .query} Urs asks: Concerning the last parenthetical remark: I suppose in this manner one could imagine $(n+1)$-categories as a foundation for $n$-categories? What happens when we let $n \to \infty$?
Toby answers: That goes in the last, as yet unwritten, section. =–
+– {: .query} Urs asks: Can you say what the problem is?
Toby answers: I'd say that it proved to be overkill; ETCS is simpler and no less conceptual. In ETCC (or whatever you call it), you can neatly define a group (for example) as a category with certain properties rather than as a set with certain structure. But then you still have to define a topological space (for example) as a set with certain structure (where a set is defined to be a discrete category, of course). I think that Lawvere himself still wants an ETCC, but everybody else seems to have decided to stick with ETCS.
Roger Witte asks: Surely in ETCC, you define complete Heyting algebras as particular kinds of category and then work with Frames and Locales (ie follow Paul Taylor’s leaf and apply Stone Duality). You should be able to get to Top by examining relationships between Loc and Set. I thought Top might be the the comma category of forgetful functor from loc to set op and the contravariant powerset functor. Thus a Topological space would consist of a triple S, L, f where S is a set, L is a locale and f is a function from the objects of the locale to the powerset of S. A continuous function from S, L, f to S’, L’, f’ is a pair g, h where g is a function from the powerset of S’ to the powerset of S and g is a frame homomorphism from L’ to L and (I don’t know how to draw the commutation square). However I think this has too many spaces since lattice structures other than the inclusion lattice can be used to define open sets.
Toby: It's straightforward to define a topological space as a set equipped with a subframe of its power set. So you can define it as a set $S$, a frame $F$, and a frame monomorphism $f\colon F \to P(S)$, or equivalently as a set $S$, a locale $L$, and an epimorphism $f\colon L \to Disc(S)$ of locales, where $Disc(S)$ is the discrete space on $S$ as a locale. (Your ’However, […]’ sentence is because you didn't specify epimorphism/monomorphism.) This is a good perspective, but I don't think that it's any cleaner in ETCC than in ETCS.
Roger Witte says Thanks, Toby. I agree with your last sentence but my point is that this approach is equally clean and easy in both systems. The clean thing about ETCC is the uniformity of meta theory and model theory as category theory. The clean thing about ETCS is that we have just been studying sets for 150 years, so we have a good intuition for them.
I was responding to your point ’ETCC is less clean because you have to define some things (eg topological spaces) as sets with a structure’. But you can define and study the structure without referring to the sets and then ’bolt on’ the sets (almost like an afterthought).
Mike Shulman: In particular cases, yes. I thought the point Toby was trying to make is that only some kinds of structure lend themselves to this naturally. Groups obviously do. Perhaps topological spaces were a poorly chosen example of something that doesn’t, since as you point out they can naturally be defined via frames. But consider, for instance, a metric space. Or a graph. Or a uniform space. Or a semigroup. All of these structures can be easily defined in terms of sets, but I don’t see a natural way to define them in terms of categories without going through discrete categories = sets.
Toby: Roger, I don't understand how you intend to bolt on sets at the end. If I define a topological space as a set $S$, a frame $F$, and a frame monomorphism from $F$ to the power frame of $S$, how do I remove the set from this to get something that I can bolt the set onto afterwards? With semigroups, I can see how, from a certain perspective, it's just as well to study the Lawvere theory of semigroups as a cartesian category, but I don't see what to do with topological spaces.
Roger Witte says If we want to found mathematics in ETCC we want to work on nice categories rather than nice objects. Nice objects in not nice categories are hard work (and probably ’evil’ to somke extent). Thus the answer to Toby is that to do topology in ETCC you do as much as possible in Locale theory (ie pointless topology) and then when you finally need to do stuff with points, you create Top as a comma like construction (ie you never take away the points but you avoid introducing them as long as possible). Is it not true that the only reason you want to introduce points is so that you can test them for equality/inequality (as opposed to topological separation)?
Mike, I spent about two weeks trying to figure out how to get around Toby’s objection ’topology’ and now you chuck four more examples at me. My gut feeling is that the category of directed graphs is found by taking the skeleton of CAT, that metric locales are regular locales with some extra condition to ensure a finite basis, that Toby can mak
[ to be continued in next comment ]
[ continuation of forwarded discussion ]
+– {: .query} Urs says: I like categorial. If we think we can improve on existing terminology we should feel free to introduce it here.
Toby responds: Once you use ’categorial’ when discussing logic, it's hard to justify using ’categorical’ in other contexts. I suppose that I could go through the whole wiki and change ’categorical’ to ’categorial’ ….
Urs says: with respect to optimal terminology I think that one problem is that the very term “category” is not optimal.
Toby responds: I think that it's too late to play Bourbaki with that. Or do you want to say ’semigroupoid’? (which occasionally appears in groupoid literature but most properly would not have identity morphisms). I got a lot of stares over dinner at Groupoidfest when I said that that might be a better term after all (for categories as algebraic objects).
Mike comments: I think it is probably too late to play Bourbaki with “categorical” as well; too many people are using it who don’t care about logic. However, there is another option here: I like to call ETCS-like theories structural set theories rather than “categori(c)al foundations”. As Lawvere and others have pointed out, ETCS is still a theory of sets; it merely differs from traditional set theories such as ZF in its lack of a global membership predicate and in what notions it takes as basic.
Toby: Can we at least say ’category-theoretic’ instead of ’categorical’? It can be very disconcerting to read, for example on tensor product, ’More categorically, this can be constructed as the coequalizer of the two maps […]’. (If anything, this is less categorical than the explicit previous construction by modding out relations, since the previous can be formalised in a membership-based set theory in which it is defined up to set-theoretic identity, while the other, however formalised, is defined only up to unique isomorphism. Of course, that should not really be considered less categorical, but it's still hardly more categorical.) To be unambiguous, this should be ’More categorially, […]’ or, if you don't like that word, ’More category-theoretically […]’. (Or do you think that ’More structurally […]’ will work here?)
Mike: At some point, I think one just has to accept that some words have more than one meaning, and learn to deal with it. I appreciate that it can be disconcerting to a logician or philosopher to read “categorical” used to mean “category-theoretic,” but it is of course just as confusing to a category-theorist when it is used to mean “having a unique model.” Undoubtedly the logicians were there first, but the time to have that argument was back when Eilenberg and Mac Lane chose the word “category.” And although I am of course biased, I think that “category-theoretic” is a more important notion in mathematics than “having a unique model.” And “categorial” looks to me like a misspelling.
Toby: Erm, no, while the term ’category’ may have some problems that one might have objected to in 1945, that was not the time to anticipate that people might later apply it to logic and then use the adjective ’categorical’. I understand why you don't like ’categorial’, so what's wrong with ’category-theoretic’ or ’structural’? (when discussing logic, that is).
Mike: I didn’t mean to say that anyone should have been able to anticipate the conflict of “categorical” related to categories with its use in logic back in 1945. I just meant that by now, when “category” has a universally established meaning, I don’t think it’s reasonable to object to the use of “categorical” to mean “related to categories.” I like “structural” when it applies, but to me it has a different meaning than “categorical”—this is the point I’m trying to make with SEAR, that structural set theory doesn’t depend on category theory. Finally, “category-theoretically” has almost twice as many syllables and letters as “categorically,” and sounds awkward.
I am sort of starting to soften towards “categorial,” at least when talking to logicians or about logic. There’s enough antagonism towards category theory in the logic/foundations community without adding to the perception that we’re stealing established terminology. But I’m not yet convinced that it’s worth going on a crusade to eliminate “categorical” referring to category theory from everyday mathematical speech.
Toby: I don't feel on a crusade, but I avoid using ’categorical’. I often used ’categorial’, or I'll use ’category-theoretic’ or ’structural’ if that seems more appropriate. (In the case of the tensor product, for example, I think that using ’structural’ gets across the idea perfectly well; if someone has already written ’categorical’ on the wiki and its seems disconcerting, then I wouldn't change it to ’categorial’ but might change it to ’category-theoretic’.) =–
[ end of forwarded discussion ]
Thanks, Urs. I have added to the foundation of mathematics (under references) backpermalink to this archived version of the old discussion. IMHO we should always keep at entries backlinks to the archived versions of removed discussions, unless they are extremely obsolete or nonsubstantial. Otherwise the discussion is lost in $n$Forum.
I think entries should only point to relevant information, not to every discussion vaguely related. I don’t think my questions to Toby from years ago in the above are relevant enough. I’d rather have them not linked from the entry. I’d rather find 5 minutes to add to the entry a nice and polished paragraph that contains the outcome of these discussions.
I do not know. Here is about 4 pages of discussion among several people, some of which is interesting and not absorbed in the entry. The purpose of references is not to point to the material identical to the entries nor necessary central to the entry but to point to expansions and further directions and related items. I do not know, I had the impression that it was not obsolete.
I just think that none of those people over the years felt that any of this was relevant or polished enough to put it into an nLab entry as usual. It sure stayed there only because everybody forgot about those discussion boxes.
Which is not to say that we should not work on that entry. That entry deserves to be improved! But it improves by adding contentful focused paragraphs, not random and unfocused chitchat. That is better had here in a discussion forum.
But it is lost if not backlinked. I think that when I get into such a discussion it absorbs about half an afternoon, so it is often a pity to loose it, from my subjective perspective. Having something idle for one year is little in comparison to the timespan of idle logs of most unfinished mathematical thoughts I usually have (I understand it might look much longer time for superquick, focused and superefficient people like you) including unfinished circles of$n$Lab entries. Backlink is about half a line, and if one has further discussion boxes in the same entry later it is likely that the person who removes that one will than archive it in the same $n$Forum spot what will once be useful. Otherwise, in long term, during the many years, the accumulated queries from one entry will be in many $n$Forum threads (( I am just talking now the matter of the principle. ))
I think I’m with Zoran here. Such discussions can be of both scientific and historical interest (providing inner thoughts and motivations which are a stimulus to many), and an unobtrusive backlink wouldn’t mar an otherwise fine (or polished) article.
The Lab-book analogy would seem to support the idea of keeping information which is useful to researchers like Zoran accessible.
I don’t think that all discussions should be linked from the page. Often, a discussion reaches some definite conclusion, which can then be incorporated into the page in a way that a future reader can obtain exactly the same information as the discussion would have provided, more easily and with less effort. However, when a discussion is not about some mathematical point and/or doesn’t reach a definite conclusion, then I think it may be valuable for a reader to be pointed to it. Probably these particular discussions are in the latter category.
I am thinking two things:
the nForum is to the nLab as what the talk-pages are on Wikipedia. On Wikipedia you’d be irritated if the Literature-section pointed you to the page’s talk-page! You want the literature section to point you to stable, relevant information.
The number of seconds it takes to choose one point of that old discusison and turn it into a short useful paragraph on the entry is comparable to the seconds it takes to link to that discussion here and then discuss that move. But the former seconds would be better invested! ;-)
Urs, with regard to point 1, my own thinking is that we should not be comparing the nLab to WP. This is not only with regard to NPOV/nPOV, but also in the idea of this being a public Lab book where we record our notes and sometimes rough thoughts (although if we are moved to work on polishing and making things look more like an encyclopedia, that can be fine as well).
Please reread the first standout box on the Home Page!
I agree with Mike that we need not indiscriminately link to every old discussion, especially those that seem like a beginner is floundering around, but more substantive discussions which did not reach a firm conclusion can be linked to in an unobtrusive way (with a flag which indicates tentativeness of the discussion, if need be). This is desirable in view of the avowed value such discussions have for researchers like Zoran.
What is the value of the discussion in this case? If it is valuable, why does nobody extract the punchline?
I think, instead, the discussion above is not valuable. I think it is confused and uninformed. Back when we had that discussion, we were all lacking the crucial insights needed to anwer that question with which I started the discussion.
I already found it embarrassing to copy that old discussion over to here. I did this only to stick to the rules. I would just entirely delete that old discussion, if I felt it was socially acceptable.
These questions: “what is the right foundation for directed homotopy theory?”, we have discussed in an informed and actually useful way elsewhere.
The value of the discussion in this case lies in the discussion itself. There is not, as far as I can see, a “punchline” which can be “extracted” from it.
Urs, as far as I can tell, there are several query boxes you removed. The first one, where you asked the question about $n$-categories, got a very brief reply from Toby. I have no issue with not linking to that.
The second was also started by you, but it seems to have to do with Lawvere’s ETCC. There the discussion does not seem confused and uninformed (strong words!) – at least participants like Toby and Mike seem not to be uninformed. How important the discussion is, that’s something we each have to decide individually, but it was probably written close to around the same time as a long discussion at the Cafe which involved Arnold Neumaier, which was of some significance I believe, and it might be useful as a way of jogging memories for people like Zoran.
The third was a discussion about ’categorial’ vs. ’categorical’, which I personally find tiresome and not very interesting. I personally wouldn’t care if that wasn’t linked back to.
But I think the real issue is this:
If it is valuable, why does nobody extract the punchline?
Well, because for one we’re busy and maybe don’t feel like dropping other work to extract punchlines! Until such time as we’re ready to break all links to an earlier discussion which may yet contain food for thought for some, why do you so strenuously object to a little unobtrusive link??
I have to go now, and not sure how much time I want to argue about this…
The third was a discussion about ’categorial’ vs. ’categorical’, which I personally find tiresome and not very interesting.
Regardless of how tiresome it is, I think there is some use in keeping it around in case someone new comes along and wants to have the same discussion. That way they can read the old discussion first and hopefully feel as though everything they wanted to say was already brought up and doesn’t need to be said again.
@Mike #15: sure, I can see that (and wouldn’t object to a link!). And I mean no disrespect who find the topic to be of interest.
I’m inclined to say that a link is warranted iff somebody thinks that a link is warranted. If Urs doubted that anybody would find the link useful, then I don’t blame him for leaving it out. If Zoran wants the link only as a matter of principle, then I wouldn’t put it in. But if Zoran (or anybody else) finds the link useful, then it should stay.
I clearly stated in post 3 “unless they are extremely obsolete or nonsubstantial” in accordance with 17. Hence I never meant that every query which is archived should be linked and I even think that they are such rare queries which do not even warrant $n$Forum archiving. Here I thought that it is substantial because it has a discussion of EETC and alike, which I have no time to comprehend at the moment but would like to relate to when in this subject next time. I also do not feel particularly strong about how to handle this or that particular entry.
Here I thought that it is substantial because it has a discussion of EETC and alike, which I have no time to comprehend at the moment but would like to relate to when in this subject next time.
So this meets the requirement in my
if Zoran (or anybody else) finds the link useful, then it should stay.
Added pointer to univalent foundations for mathematics under “Related concepts”. But this entry should really have a (small, at least) subsection on that topic.
I plan on broadening the scope of this article to talk about foundations of mathematics in general. This includes not only approaches such as ETCS which are based in category theory, but also traditional material set theories such as ZFC and Mostowski set theory, and dependent type theories like Martin-Löf type theory which do not have a separate notion of proposition from sets or types. Important concepts that should be added to this article include descriptions of the foundational notions of collection and object, the notion of membership/typing, the notion of equality of objects and equality and equivalence of collections, the notion of definition, and the basic metatheoretical foundations and deductive systems on which each foundations of mathematics are based in (natural deduction, sequent calculus, lambda-calculus, et cetera).
When I try to add $a \in A$ to the article, I get the following message:
No mapping available for Tex symbol: in
I don’t seem to have any issues on any other article, just this article.
moved material about category theory and foundations over to its own page at category theory and foundations.
Anonymous
added reference
Anonymous
1 to 27 of 27