Timeline for Delooping in homotopy type theory
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 21, 2014 at 21:33 | vote | accept | Daniel Barter | ||
| Aug 21, 2014 at 16:45 | vote | accept | Daniel Barter | ||
| Aug 21, 2014 at 16:47 | |||||
| Aug 21, 2014 at 16:43 | vote | accept | Daniel Barter | ||
| Aug 21, 2014 at 16:44 | |||||
| Aug 11, 2014 at 17:27 | comment | added | Andrej Bauer | I agree with you, of course. A major winning point for HoTT is that "$\infty$-groupoid" is just "type", and that equivalence requires no higher-dimensional conditions (which one might expect). So we do have examples where an infinite amount of higher-dimensional structure is dealt with without explicit reference to it. | |
| Aug 11, 2014 at 16:36 | vote | accept | Daniel Barter | ||
| Aug 21, 2014 at 16:43 | |||||
| Aug 11, 2014 at 11:12 | comment | added | Anton Fetisov | @AndrejBauer, personally I would be majorly disappointed if the only way to define associative algebras in HoTT were to grind through associahedra. We already have this problem in set theory. Why bother with types if the answer is the same (bar their logical usefulness)? Besides we already have a simple and complete answer in one special case: composition on loop spaces. | |
| Aug 11, 2014 at 8:19 | comment | added | Andrej Bauer | I wonder if we should give a HoTT student the task of defining associahedra in type theory. It sounds horrible. | |
| Aug 10, 2014 at 21:36 | history | answered | Anton Fetisov | CC BY-SA 3.0 |