[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.