Timeline for Are paths in HoTT perhaps just "cost-free" paths?
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5, 2013 at 12:03 | comment | added | Urs Schreiber | Sorry about the "free", should have said "presentable". Fixed now. | |
| Nov 5, 2013 at 12:03 | history | edited | Urs Schreiber | CC BY-SA 3.0 |
added 119 characters in body
|
| Nov 5, 2013 at 6:08 | comment | added | Mike Shulman | No, it's not in principle straightforward. There are coherence issues. On the other hand, HITs don't just present free $\infty$-monads; indeed the capability to present non-free monads is more or less what distinguishes HITs from ordinary inductive types. | |
| Nov 4, 2013 at 18:53 | history | answered | Urs Schreiber | CC BY-SA 3.0 |