HoTT doesn’t blur those distinctions — it formalizes the distinction.
The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.
The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)
> ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
Counterpoint: no it doesn’t, because almost every working mathematician uses a higher level type theory in their work that “compiles” to ZFC and will run away screaming if you try to make them compile their work down to formal ZFC statements because set theory is a garbage foundation — the worst of the three options.
“My axioms do everything but formalize proofs!” is the equivalent of “my car does everything but drive!”