Timeline for When to use coinductive types?
Current License: CC BY-SA 4.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 1, 2022 at 15:12 | comment | added | Mike Shulman | @მამუკაჯიბლაძე Not that I know of; that work in Coq was sort of stalled a while ago, but mainly because it wasn't clear whether it was the most practical version. Simplicial sets don't work, as far as anyone knows. And saying "infinite-dimensional categories" is maybe a bit misleading to people who actually know what that means -- it's not known how to get all the coherence, only finite fragments of it. | |
| Apr 1, 2022 at 10:20 | comment | added | მამუკა ჯიბლაძე | Last example: wow! Is there some text to read about this in more detail? I mean, how to actually work with it, and also whether one can similarly define other things like simplicial sets, etc? | |
| Feb 9, 2022 at 19:30 | history | answered | Mike Shulman | CC BY-SA 4.0 |