Timeline for Are simplicial sets the intended model of HoTT?
Current License: CC BY-SA 3.0
9 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Apr 13, 2017 at 12:58 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
Jul 11, 2013 at 14:54 | comment | added | François G. Dorais | @Andrej: In your last sentence, do you mean something specific by "non-standard" homotopy? | |
Jul 11, 2013 at 11:25 | comment | added | Andrej Bauer | @RonnieBrown: I think so. It is clear that there are variants of identity types which give slightly different higher-dimensional structure. The standard identity types naturally lead to globular structure, but one can imagine $n$-fold identity types that will make things look more like simplices. I think some people are experimenting, but it's hard to replace an entrenched theory. I think similar situation arises with "non-standard" homotopy. | |
Jul 11, 2013 at 10:39 | comment | added | Ronnie Brown | I'll add my standard comment that things have been done in homotopy theory with cubical sets (with connections) and also with $n$-fold groupoids, which have not been achieved with simplicial sets, mainly because of the ease of considering multiple compositions. Could this have implications for HoTT? | |
Jul 11, 2013 at 7:54 | answer | added | Andrej Bauer | timeline score: 13 | |
Jul 11, 2013 at 6:24 | answer | added | Neil Strickland | timeline score: 11 | |
Jul 11, 2013 at 1:52 | comment | added | François G. Dorais | No, that's the first question. If there is an intended model it's surely simplicial sets. | |
Jul 11, 2013 at 1:49 | comment | added | Qiaochu Yuan | Is it clear that HoTT has an intended model? My vague impression is that HoTT can serve as an internal language for various kinds of higher categories and that it wasn't intended to describe just one such category. | |
Jul 11, 2013 at 1:25 | history | asked | François G. Dorais | CC BY-SA 3.0 |