Timeline for What's the point of cubical type theory?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 6, 2019 at 4:10 | comment | added | Kaa1el | @AndrejBauer Sorry for the ambiguity. It was my mistake to take HoTT and CTT as a whole. | |
| Mar 20, 2019 at 12:43 | comment | added | Andrej Bauer | You're questioning the role of cubical type theory as a foundation of mathematics, but have you heard or read any of its authors claim that it is such a foundation in the first place? Certainly such claims were made about HoTT/UniMath (as witnessed by the subtittle of the HoTT book), but for cubical type theory I am not aware of such claims. | |
| S Mar 20, 2019 at 9:51 | history | suggested | user64494 | CC BY-SA 4.0 |
A typo in the title is corrected.
|
| Mar 20, 2019 at 9:12 | review | Suggested edits | |||
| S Mar 20, 2019 at 9:51 | |||||
| Mar 20, 2019 at 8:43 | history | edited | Kaa1el | CC BY-SA 4.0 |
deleted 3 characters in body
|
| Jul 22, 2018 at 5:51 | comment | added | Mike Shulman | FWIW, some of us working in HoTT (myself included) have similar reservations. Finding some normalizing type theory in which univalence holds is undoubtedly a great advance. But I don't think the extant cubical type theories are "the answer" yet, for the reasons you mention as well as others (to name a few: the beauty of generating all oo-groupoid structure from the simple J-rule is lost; paths in the universe are not literally equivalences, but generated by "glue" types; and many/most model categories of cubical sets apparently do not present the homotopy theory of oo-groupoids). | |
| Jul 20, 2018 at 0:13 | comment | added | Kaa1el | found a similar topic on reddit Haskell: reddit.com/r/haskell/comments/561muo/… | |
| Jul 19, 2018 at 17:19 | comment | added | Bas Spitters | This paper argues that cubical methods are useful even in regular HoTT. So, cubical type theory can be seen as just explicating this fact. dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf | |
| Jul 19, 2018 at 11:53 | comment | added | Yemon Choi | @LSpice Shush :) | |
| Jul 19, 2018 at 11:50 | comment | added | LSpice | @SimonHenry, I think it is irresistible now to post regarding other things that are only a model. :-) | |
| Jul 19, 2018 at 9:30 | comment | added | Simon Henry | I feel like there is something more to be said here (and I don't know what it is): One has a cubical model of type theory with univalence which is constructive/computable. But its only a model, that does not explain why one wants to define a new type theory because of that model. For example, When Voevodsky constructed the Simplicial model of type theory nobody went one to define "simplicial type theory". | |
| Jul 19, 2018 at 1:37 | comment | added | David Roberts♦ | The rough point of cubical type theory is that it is computable: the univalence axiom failed to compute in other, earlier, approaches. Not to mention that the one can develop fully constructive models of the cubical type theory, which is harder than it sounds, since one needs to constructively give a model category structure, and that is only a more recent mathematical advance. | |
| Jul 19, 2018 at 0:52 | review | Close votes | |||
| Jul 25, 2018 at 3:02 | |||||
| Jul 19, 2018 at 0:52 | comment | added | Nik Weaver | I agree, though in the past mathoverflow has been fairly tolerant of questions bordering on philosophy of mathematics. FWIW I'd be interested in seeing some answers to this question. | |
| Jul 19, 2018 at 0:40 | history | edited | Kaa1el |
edited tags
|
|
| Jul 19, 2018 at 0:35 | comment | added | LSpice | This seems like very much a question about the philosophy of mathematics, rather than a problem in research mathematics. | |
| Jul 19, 2018 at 0:12 | history | asked | Kaa1el | CC BY-SA 4.0 |