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)