Timeline for HoTT without Funext, Univalence
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 6, 2016 at 5:50 | vote | accept | H Koba | ||
| Sep 5, 2016 at 15:12 | comment | added | H Koba | Thanks, Peter and @mike-shulman. I mean models of ITT without univalence or funext, and "good old-fashioned set model" in Peter's answer and ones in Mike's answer are what I want. I shouldn't have used the word "HoTT". | |
| Sep 4, 2016 at 17:36 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 3.0 |
clarified wording
|
| Sep 4, 2016 at 15:57 | comment | added | Mike Shulman | However, there are also models in which UIP and univalence, and even function extensionality, all fail. For instance, the projective model in Z/2-groupoids in arxiv.org/abs/1512.04083 . A less esoteric possibility is the strict $\infty$-groupoid model in mawarren.net/papers/crmp1295.pdf, though I don't recall whether it's been checked that univalence fails there (though IIRC we don't expect it to). | |
| Sep 4, 2016 at 13:00 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 3.0 |