24
$\begingroup$

I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy theory really differentiate it from the old good set theory approach. Now with the new cubical syntax I started question it as a tool to serve the foundation of mathematics. To me, it no longer has the appeal that everything is minimalist. Shouldn't a foundation be simple enough with only a few things to start with? Not a lot students are going to study mathematics in such a way that equality is some infinity groupoid and you need to do box filling and glueing stuffs before knowing how to do linear algebra or calculus. I understand that doing cubical type theory is to give computational meaning to the univalent axiom but even if we ever prove its decidability and normalization, we are not getting a simple and minimal system to serve as foundation of mathematics.

Please correct my view if I am wrong (I am not a mathematician, just working as a programmer for some tech firms). I really like the way type theory bridging programming with mathematics but failed to see the univalent approach can serve as a foundation. Does a type system with minimal content as a foundation of mathematics ever exist? Will there be day when mathematician doing their work by writing code in some type system framework just like nowadays programmer?

Any literature regarding this problem is welcomed, thanks a lot for reading through! (probably nonsense to you guys lol)

Improve this question
$\endgroup$
11
  • 10
    $\begingroup$ 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. $\endgroup$
    – Nik Weaver
    Commented Jul 19, 2018 at 0:52
  • 5
    $\begingroup$ 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. $\endgroup$
    – David Roberts ♦
    Commented Jul 19, 2018 at 1:37
  • 4
    $\begingroup$ @SimonHenry, I think it is irresistible now to post regarding other things that are only a model. :-) $\endgroup$
    – LSpice
    Commented Jul 19, 2018 at 11:50
  • 11
    $\begingroup$ 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). $\endgroup$
    – Mike Shulman
    Commented Jul 22, 2018 at 5:51
  • 7
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Mar 20, 2019 at 12:43

0

Reset to default

You must log in to answer this question.