Hacker News Reader

They are almost certainly aware of Mizar. Mizar's foundation is ZFC+Tarski's axiom. If you are developing a foundation based on homotopy theory/type theory you probably don't care about results formalized in Mizar. Also the type theory people in general prefer constructivist mathematics, and would reject Axiom of Choice and friends being in the foundation.

View on HN

But doesn't Mizar void the argument that we need a new foundation as set theory has not been conducive to mechanized proofs?

I don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.

"Prettier" is subjective.

Absolutely. Never claimed otherwise.

I think this is right (not an HoTT expert), it voids it. I'd say that what type theory brings in, that didn't come for free in set theory (ZFC or Mizar's Tarski-Grodendiek extension), is the Curry-Howard correspondence that has the slogan "propositions as types, proofs as programs". With that correspondence you can see the same thing as a program (in a typed lambda calculus depending of the type theory of interest), or as a proof in a corresponding logic.

Reply on news.ycombinator.com