You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

Douglas_Knight comments on Open thread, 24-30 March 2014 - Less Wrong Discussion

6 Post author: Metus 25 March 2014 07:42AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (156)
Tags: open_thread

Comments (156)

You are viewing a single comment's thread. Show more comments above.

Comment author: khafra 28 March 2014 04:43:26PM 1 point [-]

Apparently, founding mathematics on Homotopy Type Theory instead of ZFC makes automated proof checking much simpler and more elegant. Has anybody tried reformulating Max Tegmark's Level IV Multiverse using Homotopy Type Theory instead of sets to see if the implied prior fits our anthropic observations better?

Comment author: Douglas_Knight 29 March 2014 09:56:15PM 2 points [-]

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.

Comment author: khafra 31 March 2014 11:24:30AM *  0 points [-]

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

Powered by Reddit Powered by Reddit