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 highe
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Duration set to six days to encourage Monday as first day.