Timeline for Categorical semantics of universe levels in dependent type theory
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 6, 2021 at 19:08 | answer | added | varkor | timeline score: 4 | |
| May 1, 2021 at 2:11 | comment | added | Mike Shulman | At an elementary level, there isn't going to be an answer to this other than something like "LCCs with universes". More interestingly, there are non-elementary ways to construct universes, e.g. in Grothendieck toposes if there are inaccessible cardinals in the ambient set theory. Is that the sort of thing you're interested in? | |
| May 1, 2021 at 1:37 | comment | added | David Roberts♦ | What are you assuming about the universes? Just closure under $\Pi$? | |
| Apr 30, 2021 at 16:02 | review | First posts | |||
| Apr 30, 2021 at 16:40 | |||||
| Apr 30, 2021 at 15:57 | history | asked | mfddnjk2 | CC BY-SA 4.0 |