[teilo]

I agree regarding the completeness of type theory in regards to Turing computability.

But I disagree regarding paradoxes in ZFC. Russel's paradox specifically applies to naive (simple Cantor) set theory, something the ZFC was explicitly designed to address with its axioms of choice and infinity. Furthermore the HoTT is itself expressible in the common extension of ZFC which adds at least one inaccessible cardinal.

And, mathematically speaking, the ZFC excels in dealing with infinities, which is more difficult (though possible) in the various type theories.

[hiker]

I agree with everything besides your stated difficulties with infinities in type theory. Here's one infinity

  inductive ℕ : Type
  | zero : ℕ
  | succ (n : ℕ) : ℕ

the type of natural numbers with cardinality ℵ₀. Here' s a bigger infinity:

  ℕ → ℕ

the type of functions over natural numbers.

From then on one can start talking about different injective functions between those types and infer cardinality of which is bigger and so forth and so forth.

It's values, types and functions all the way down. Nothing from ZFC is lost, on the bright side, your proofs are checked by a computer. On an even brighter side, your proofs can be semi-automated, even brute forced.