Timeline for What kind of category is generated by Cubical type theory?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 27, 2018 at 12:38 | history | edited | Ali Caglayan | CC BY-SA 4.0 |
changed heyting to de morgan as it is technicaly wrong
|
| Jun 1, 2018 at 23:30 | vote | accept | Ali Caglayan | ||
| May 31, 2018 at 3:52 | comment | added | user40276 | @MikeShulman You're right. But I was not trying to answer the question. It's just the model of cubical sets. Now that I reread my comment, it's indeed ambiguous or even plainly wrong the way it's written. I should have said "One 1-categorical presentation..." instead. | |
| May 30, 2018 at 16:29 | comment | added | Mike Shulman | @user40276 I don't think that answers the question: that paper constructs one specific model in the category of cubical sets, whereas the question is about what general class of categories admit models. | |
| May 30, 2018 at 1:17 | comment | added | user40276 | The 1-categorical presentation of the categorical semantics of cubical type theory is described in section 8 of hal.inria.fr/hal-01378906/document | |
| May 29, 2018 at 18:04 | answer | added | Mike Shulman | timeline score: 18 | |
| May 29, 2018 at 15:48 | answer | added | Simon Henry | timeline score: 9 | |
| May 29, 2018 at 15:39 | history | edited | Ali Caglayan | CC BY-SA 4.0 |
spelling
|
| May 29, 2018 at 15:32 | history | asked | Ali Caglayan | CC BY-SA 4.0 |