Timeline for Elementary theory of the category of groupoids?
Current License: CC BY-SA 4.0
30 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 20, 2021 at 4:49 | vote | accept | CommunityBot | ||
| Apr 12, 2021 at 10:40 | answer | added | Mike Shulman | timeline score: 9 | |
| Apr 12, 2021 at 10:16 | comment | added | Mike Shulman | Just found this. (If you want to actually ping/summon someone, you need to use an @.) Starting with the most recent coment, the relation between pseudolimits and PIE-limits is that every pseudolimit is a PIE-limit but not conversely. I'm dubious of a claim that one can construct all pseudolimits from pseudoterminal objects and pseudopullbacks; I would only expect that to work with fully weak bilimits (but it certainly does in that case). | |
| Feb 14, 2021 at 11:18 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
small clarification on what the question is after
|
| Feb 4, 2021 at 16:25 | answer | added | Andrej Bauer | timeline score: 9 | |
| Feb 4, 2021 at 15:47 | history | edited | user173426 | CC BY-SA 4.0 |
added 646 characters in body
|
| Feb 4, 2021 at 5:35 | history | edited | user173426 | CC BY-SA 4.0 |
added 178 characters in body
|
| Feb 4, 2021 at 4:09 | history | edited | user173426 | CC BY-SA 4.0 |
deleted 62 characters in body
|
| Feb 4, 2021 at 4:03 | history | edited | user173426 | CC BY-SA 4.0 |
added 55 characters in body
|
| Feb 4, 2021 at 3:20 | comment | added | Tim Campion | But an often more convenient way to work with (2,1) limits is to construct them from products, iso-inserters, and equifiers -- so called PIE limits. The precise relationship to pseudolimits is not something I have at my fingertips, but they should be essentially equivalent. | |
| Feb 4, 2021 at 3:18 | comment | added | Tim Campion | In the $(2,1)$-case the situation is terminologically a little awkward. There is a strict notion of limit which still exists if you're working with strict (2,1)-categories (which it is often convenient to do) which is defined up to isomorphism, and there is also a weak notion of (2,1)-limit, which should really be defined only up to equivalence, but can also be given an up-to-isomorphism definition as a pseudolimit. The analog of the statement in question is that a (2,1)-category with a pseudoterminal object and pseudopullbacks has all finite pseudolimits up to equivalence. | |
| Feb 4, 2021 at 3:11 | comment | added | Tim Campion | @MadeleineBirchfield Regarding the edit: I'm not sure what "saturated" means here. Every category with a terminal object and pullbacks has finite limits. This is also true $\infty$-categorically. The caveat is that a finite 1-category need not be finite when regarded as an $\infty$-category! | |
| Feb 4, 2021 at 3:02 | history | edited | user173426 | CC BY-SA 4.0 |
added 514 characters in body
|
| Feb 4, 2021 at 1:50 | comment | added | Tim Campion | @YCor I'll just point out that the capitals in the title seemed appropriate to me by analogy with Lawvere's Elementary Theory of the Category of Sets. I don't have terribly strong feelings about it though. | |
| Feb 4, 2021 at 1:49 | comment | added | Tim Campion | @MadeleineBirchfield That's a good point. For that the canonical place to point you would be Makkai's FOLDS. | |
| Feb 4, 2021 at 1:36 | history | edited | user173426 |
edited tags
|
|
| Feb 4, 2021 at 0:11 | comment | added | user173426 | One thing that might be necessary is to replace the notion of equality in the first order logic with a notion of natural isomorphism, as two functors are no longer said to be equal to each other, but rather only naturally isomorphic to each other. | |
| Feb 3, 2021 at 21:56 | comment | added | Tim Campion | Yeah, I'm kinda hoping he'll drop by. | |
| Feb 3, 2021 at 21:55 | comment | added | Harry Gindi | @TimCampion Maybe someone will ping Mike Shulman for an answer here. I bet he knows how to do it. | |
| Feb 3, 2021 at 20:48 | comment | added | Tim Campion | And I'm reasonably certain that there are papers out there studying type theory with a 1-truncaction axiom. The analog of the issue in the last paragraph of my answer in this setting is that you have to figure out what form of univalence you'll have. | |
| Feb 3, 2021 at 20:31 | comment | added | Noah Snyder | Or rather, that should work if you interpret “category of groupoids” to mean “(2,1)-category of groupoids” | |
| Feb 3, 2021 at 20:23 | comment | added | Noah Snyder | I'm nervous to try to write up the answer myself because I'll mess up something about universes, but this is the sort of thing that should be pretty straightforward if you understand the HoTT book and ETCS. You want to do the same kind of translation that relates Martin-Löf type theory with Axiom K (i.e. all types are 0-truncated) to ETCS but instead applied to type theory with a 1-truncation axiom. | |
| Feb 3, 2021 at 19:05 | comment | added | Tim Campion | I just remember that when I read Lawvere's paper (The Category of Categories as a Foundation for Mathematics), although I couldn't make an informed decision about whether it could found category theory, it immediately felt to me that the axioms did not feel "natural" in a way that foundational axioms should but rather like some sort of "encoding" of things. That's the primary reason that I personally have trouble taking it seriously foundationally. | |
| Feb 3, 2021 at 19:03 | comment | added | Tim Campion | @HarryGindi You may be right -- I don't remember the details. However, I believe something similar can be said about ETCS -- it's not clear that Lawvere initially appreciated that the theory did not entail anything like the axiom scheme of replacement in ZFC. Perhaps the issues with ETCC are even more serious, but today you'll still find arguments that ETCS, though substantially weaker than ZFC, is still adequate for "most of mathematics". In fact, just the other day Colin McLarty reiterated that everything Grothendieck ever did fits into ETCS. | |
| Feb 3, 2021 at 18:58 | answer | added | Tim Campion | timeline score: 3 | |
| Feb 3, 2021 at 18:57 | comment | added | Harry Gindi | @TimCampion My understanding is that ETCC is largely a theory that failed to provide a good basis for category theory. Very early after Lawvere's paper about it, it was shown that it was unable to prove very simple mathematical statements, so in that sense, it's a 'failed mathematical theory'. On the other hand, you could maybe try to axiomatize a 1-bounded version of HoTT. | |
| Feb 3, 2021 at 18:16 | history | edited | user173426 | CC BY-SA 4.0 |
added 31 characters in body
|
| Feb 3, 2021 at 17:48 | history | edited | YCor | CC BY-SA 4.0 |
removed capitals from title
|
| Feb 3, 2021 at 17:45 | history | edited | user173426 | CC BY-SA 4.0 |
added 7 characters in body
|
| Feb 3, 2021 at 17:14 | history | asked | user173426 | CC BY-SA 4.0 |