Timeline for Uniqueness of comparison functors
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 11, 2022 at 16:03 | comment | added | Mike Shulman | If you're referring to your construction of the functor Force in that other question, it's already written (like nearly all mathematics) in "informal dependent type theory", so there's nothing to worry about: of course it's insensitive to how you define categories. | |
| Mar 11, 2022 at 16:01 | comment | added | Mike Shulman | Category theory is (among other things) a language for talking about questions in other subjects, applicable to set theory as well as to group theory. This doesn't mean that all questions about set theory can be phrased using category theory; but when you do use that language you should use it correctly, regardless of the subject. | |
| Mar 11, 2022 at 16:00 | comment | added | Mike Shulman | You're free to believe forcing to be "more fundamental" than group theory. My point was just that the fact that questions about forcing phrased in categorical language haven't been asked by non-set-theorists says no more about whether those questions can be posed in the correct dependently typed language of category theory than the fact that questions about group theory phrased in categorical language haven't been asked by non-group-theorists says anything analogous about those questions. | |
| Mar 11, 2022 at 10:19 | comment | added | Alec Rhea | I consider forcing (and related notions of 'moving between universes') more fundamental to 'how the multiverse is' in that pseudoreligious sense than things studied by group theorists etc., though, and so gain more by viewing things set theoretically than I would viewing them e.g. group theoretically. | |
| Mar 11, 2022 at 10:18 | comment | added | Alec Rhea | To further beat a dead horse: how does this square with Peter's answer asserting an equivalence between the categories of categories with disjoint hom-sets and the category of categories with possibly non-disjoint hom-sets (also mentioned on the nlab)? Does my argument work 'up to equivalence', so my intuition is already correct 'up to equivalence'? | |
| Mar 7, 2022 at 16:01 | comment | added | Mike Shulman | Of course questions about forcing are more thoroughly explored and cared about by the set theory community. Questions about group theory are also more thoroughly explored and cared about by the group theory community, etc. etc. That doesn't have anything to do with whether the questions can be formulated in a type-theoretic foundation. | |
| Mar 7, 2022 at 15:59 | comment | added | Mike Shulman | Granted, the difference between type theory and material set theory is not as extreme as that between high-level programming languages and assembler, although part of that is because in practice mathematicians don't usually actually use material set theory but rather an informal type-theory-like layer built on top of it. But it matters, not just to rule out questions like this, but especially when teaching students who haven't yet internalized that informal layer. | |
| Mar 7, 2022 at 8:57 | comment | added | Alec Rhea | Probably nothing but ignorance on my part would prevent me from posing them, but I do feel (perhaps due to more ignorance) that those notions are more thoroughly explored and cared about by the set theory community -- I have never seen a question posed about forcing from a type theorist, but a brief googling did turn up some material so maybe I'm just wrong. | |
| Mar 7, 2022 at 8:55 | comment | added | Alec Rhea | Touché on the programming language metaphor (although we are now humans thinking like computers as I feared); more seriously, do you really feel like material set theories with a global membership predicate are as difficult to work with as programming in compiler would be? I find the ' disorganized mélange of concepts' immediately present in a material set theory to be a boon in the sense that I can 'see how to define what I want', and categories in turn arrange the mélange into a beautiful hierarchy. | |
| Mar 7, 2022 at 7:33 | comment | added | Mike Shulman | What makes you think there would be any difficulty in posing those questions type-theoretically? | |
| Mar 7, 2022 at 7:32 | comment | added | Mike Shulman | Yes, you can avoid making type errors when you program with assembly language, but it's much easier to avoid them if you use a language whose compiler will catch them for you. | |
| Mar 7, 2022 at 6:32 | comment | added | Alec Rhea | there are still questions that have occurred to me thinking set-theoretically about category theory that I don't even see how to pose type theoretically, let alone answer them. | |
| Mar 7, 2022 at 6:31 | comment | added | Alec Rhea | It indicates that I wasn't listening hard enough to my intuition for what the set-theoretical universe looks like; I've idly considered the fact that the ordered pairs definition of a function is somewhat ambiguous on what its codomain is, and I've idly considered that there are a proper class of options for any function, but I never put 2 and 2 together to realize that we effectively have a proper class of copies of each function. If I had walked out the few extra steps the error in my intuition would have become clear with no need for types, and (cont.) | |
| Mar 7, 2022 at 4:53 | comment | added | Mike Shulman | And it doesn't help that thinking set-theoretically is what led you to make the mistake in this question, while thinking type-theoretically it wouldn't even have entered your awareness? | |
| Mar 7, 2022 at 2:01 | comment | added | Alec Rhea | As much as I've been keenly awaiting the day that type theory feels like a more natural foundation than set theory, constantly expecting it around each new bend I take deeper into category theory, I am still left with the feeling that I would only prefer type theory if I were a computer or a human who needed to think similarly to a computer. There is something about set theory that captures my nascent intuition for 'how things should be in the multiverse' in a way that feels almost like religion; I do still eagerly await the day type theory feels the same. | |
| Mar 5, 2022 at 17:33 | comment | added | Mike Shulman | I would say the correct definition of "a function" includes its domain and codomain. Otherwise what is its type? It's only in the weird world where everything is unnaturally encoded in terms of a global membership predicate like that of ZFC that you can even talk about an abstract "set of ordered pairs" without first specifying what sets the components of those pairs are to be drawn from. (-:O | |
| Mar 5, 2022 at 14:30 | comment | added | Alec Rhea | Ah, so we really do have to think about there being a proper class of copies of each function in ${\bf Set}$ since the the codomain of each function has a proper class of supersets; I find that hilarious. | |
| Mar 5, 2022 at 8:55 | comment | added | Mike Shulman | A protocategory is more or less an archaic set-theoretic way to approximate the natural dependently typed definition. | |
| Mar 5, 2022 at 8:54 | comment | added | Mike Shulman | A category only has a domain and codomain function when you use the one-collection-of-morphisms definition of category. But in practice, such as when defining the EM category, we generally use the dependently typed definition of category. It's easy to make the latter definition into the former by taking a disjoint union of the homsets, but there's rarely any point to that. | |
| Mar 5, 2022 at 5:36 | comment | added | Alec Rhea | But wait, how does this square with the fact that a category has a domain and codomain function, sending each arrow to ‘it’s domain and codomain’? Is the EM category a protocategory and not a category, and if so is there a way to canonically obtain a category out of a protocategory? | |
| Mar 3, 2022 at 14:52 | comment | added | Alec Rhea | Thank you, this makes explicit the uneasy feeling I had about this argument. | |
| Mar 3, 2022 at 14:51 | vote | accept | Alec Rhea | ||
| Mar 3, 2022 at 14:50 | history | answered | Mike Shulman | CC BY-SA 4.0 |