Timeline for Are simplicial sets the intended model of HoTT?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 12, 2013 at 14:58 | comment | added | Andrej Bauer | I defer to the expert. | |
| Jul 11, 2013 at 22:21 | comment | added | Mike Shulman | @FrançoisG.Dorais, I would say that yes, absolutely, all $(\infty,1)$-toposes are univalent. The problem is to find definitions of "$(\infty,1)$-topos" and "univalent" which make this true, but this is only a technical problem --- intuitively, we have a pretty good idea of what both mean. It's true that at present we don't know how to model the usual strict form of univalence in all Grothendieck $(\infty,1)$-toposes (which are the only ones that have a precise definition at the moment), but there are weaker forms of univalence that do hold. | |
| Jul 11, 2013 at 22:18 | comment | added | Mike Shulman | This is a much fairer and more even-handed answer than I would have been able to give. (-: Personally, despite those long and thought-provoking discussions at IAS, I am still surprised that in the 21st century anyone uses the phrase "intended model" any more. Are the integers the "intended abelian group"? | |
| Jul 11, 2013 at 16:38 | comment | added | Andrej Bauer | No, no, it seems that one has to work to get univalence. At present we lack techniques to fabricate univalent models of various kinds. But if we discount univalence, there is still the question on how type theory and higher toposes fit together. | |
| Jul 11, 2013 at 13:22 | comment | added | François G. Dorais | Thanks, Andrej! This confirms some of my initial impressions. Regarding the categorical logic perspective, despite the fact that this hasn't been fully worked out, is there a clear feeling what the intended class of models is from that point of view? Are all $(\infty,1)$-toposes univalent? | |
| Jul 11, 2013 at 12:25 | comment | added | Urs Schreiber | An intended model for HoTT seems like a rather sad idea. It's like the Vikings discovering America but then rather intending to go back home after all. | |
| Jul 11, 2013 at 8:33 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
deleted 3 characters in body
|
| Jul 11, 2013 at 7:54 | history | answered | Andrej Bauer | CC BY-SA 3.0 |