> 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

> 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. Exactly this, thanks!