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 10, 2021 at 18:34 | comment | added | Paul Taylor | For categories with display maps, Chapter VIII of my book is a much better account. For universes, the Andy Pitts' paper on Russell's paradox that also has my name on it, is probably the best early reference. | |
| May 6, 2021 at 19:28 | history | edited | varkor | CC BY-SA 4.0 |
added 243 characters in body
|
| May 6, 2021 at 19:21 | comment | added | varkor | @PaulTaylor: I should have thought to look there, thanks! I shall add a reference imminently. | |
| May 6, 2021 at 19:16 | comment | added | Paul Taylor | Somebody introduced categories with display maps and this definition of universes in his thesis in 1987. | |
| May 6, 2021 at 19:08 | history | answered | varkor | CC BY-SA 4.0 |