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 Tarsk

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.