Hacker News Reader

I understand your last sentence to agree with the statement that everything could be formalized in ZFC given sufficient effort. (I do not really care by what means we know this can be done.) If so, then I'm not sure why you disagree with what I wrote previously.

View on HN

> everything could be formalized in ZFC given sufficient effort

Since I'm not sure what could be comprised under "everything", I don't think I can agree with that statement. The whole point of "practical" formalization efforts is to add some rigor to such assertions. And you've acknowledged that type theoretical foundations can be useful to practitioners, so what's it exactly that you disagree about?

The disagreement is about whether there are reasons aside from facilitating formalization to care about HoTT. (Because if not, it seems like we should all be jumping on the Lean bandwagon instead.)

Reply on news.ycombinator.com