> ZFC is the x86 assembly language of foundations.
> The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics
> Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.
> The goals of (homotopy) type theory are very different: they are trying to be suitable for actually doing modern mathematics
> Only foundations people care about ZFC, and the kind of foundations that the ZFC people care about is irrelevant to the practice of general mathematics.
Exactly this, thanks!