In a practical sense, hasn't type theory already replaced ZFC in the foundations of math? Lean is what working mathematicians currently use to formally prove theorems, and Lean is based on type theory rather than ZFC.
From https://news.ycombinator.com/item?id=42440016#42444882 :
> /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4
https://github.com/forked-from-1kasper/ground_zero :
> Lean 4 HoTT Library