Timeline for What is realignment and is it useful in non-univalent theories?
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 6, 2023 at 16:03 | comment | added | Trebor♦ | Updated broken link. | |
| Aug 6, 2023 at 16:03 | history | edited | Trebor♦ | CC BY-SA 4.0 |
deleted 11 characters in body
|
| Mar 4, 2022 at 23:28 | comment | added | Mike Shulman | Yes, WISC follows from the presentation axiom, which holds in any free exact completion. | |
| Mar 3, 2022 at 11:35 | vote | accept | Trebor♦ | ||
| Mar 3, 2022 at 10:54 | comment | added | Jonathan Sterling | @UlrikBuchholtz Yes, thanks for the clarification! I am thinking of "predicative topos" which usually assumes WISC or something like it. (Btw onlookers should note that WISC is not too scary! I believe it holds in setoids, for instance, even if it is false for presets.) | |
| Mar 3, 2022 at 10:53 | comment | added | Ulrik Buchholtz | AFAIK, sheafification only exists in a constructive and predicative metatheory if we assume WISC. But perhaps that's what you meant. | |
| Mar 3, 2022 at 10:38 | comment | added | Jonathan Sterling | So the contribution of the new work is to show that we can get very very strict universes in sheaf topoi, as opposed to the past when we knew how to get only universes satisfying various laws up to isomorphism. | |
| Mar 3, 2022 at 10:38 | comment | added | Jonathan Sterling | Btw one thing I wanted to make clear for a long time is, there was never any problem with having non-cumulative universes in sheaf topoi even constructively --- so long as you are OK with the connectives for each universe having their own introduction and elimination forms, rather than having these be coherently chosen for the whole hierarchy. It is a shame that in the literature several people cast doubt on whether universes exist in sheaf topoi --- as Streicher showed, one has them immediately as soon as sheafification exists, but that works even in a constructive and predicative metatheory. | |
| Mar 3, 2022 at 10:11 | comment | added | Jonathan Sterling | @Pierre-MariePédrot Thanks, I'm glad you're interested! I am also unsatisfied with how much hard category theory this involves... If we had succeeded in a constructive version, then I think it would have had a shape that is more comprehensible to you. Let me say morally what this is: the universe construction is "essentially" (but not actually) a "higher inductive-recursive" universe in which the inductive constructors are just freely adding in solutions to ALL realignment problems (as opposed to adding in specified connectives like in a usual IR universe). | |
| Mar 3, 2022 at 9:59 | comment | added | Pierre-Marie Pédrot | I've been obsessed with universes in sheaf topoi recently. I'm happy to see that you solved the problem, even non-constructively. Unfortunately, I am not really able to make sense of your paper because I just don't understand categorical-speak, especially when it comes to dependent types. Would it be possible to get a translation for the ignorant masses? | |
| Mar 3, 2022 at 9:40 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
mention WISC
|
| Mar 3, 2022 at 8:49 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
Better heading
|
| Mar 3, 2022 at 8:42 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
give a bit more detail why the cumulativity thing is important
|
| S Mar 3, 2022 at 8:36 | review | First answers | |||
| Mar 3, 2022 at 9:32 | |||||
| S Mar 3, 2022 at 8:36 | history | answered | Jonathan Sterling | CC BY-SA 4.0 |