> How can roots be changed without a redo of the universe?
This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article.
His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.
This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article.
His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.