Homotopy type theory differs from ZFC in two ways. One way is that it, like ordinary type theory, is constructive and ZFC is not. The other is that it is based in homotopy theory. It is that latter property which makes it well suited for proofs in homotopy theory (and category theory). Most of the examples in slides you link to are about homotopy theory.
Tegmark is quite explicit that he has no measure and thus no prior. Switching foundations doesn’t help.
It is that latter property which makes it well suited for proofs in homotopy theory (and category theory). Most of the examples in slides you link to are about homotopy theory.
I found a textbook after reading the slides, which may be clearer. I really don’t think their mathematical aspirations are limited to homotopy theory, after reading the book’s introduction—or even the small text blurb on the site:
Homotopy type theory offers a new “univalent” foundation of mathematics, in which a central role is played by Voevodsky’s univalence axiom and higher inductive types. The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning
Homotopy type theory differs from ZFC in two ways. One way is that it, like ordinary type theory, is constructive and ZFC is not. The other is that it is based in homotopy theory. It is that latter property which makes it well suited for proofs in homotopy theory (and category theory). Most of the examples in slides you link to are about homotopy theory.
Tegmark is quite explicit that he has no measure and thus no prior. Switching foundations doesn’t help.
I found a textbook after reading the slides, which may be clearer. I really don’t think their mathematical aspirations are limited to homotopy theory, after reading the book’s introduction—or even the small text blurb on the site: