Skip to main content
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