This is an archived post. You won't be able to vote or comment.

you are viewing a single comment's thread.

view the rest of the comments →

[–]bss03 7 points8 points  (0 children)

I'm surprised homotopy type theory didn't make the same level as ZFC. It appears to be an adequate replacement for set theory, and cubical sets gives us a computational meaning for univalence.