> Actually, Metamath is not tied to ZFC. As the name implies it is a meta-theory where you could implement a lot of different theories. That said, most Metamath developments use ZFC. I haven’t seen anyone doing type theory in Metamath, but from what I understand it may be possible.

That's true. There's a Metamath database that encodes Higher-Order Logic (HOL) aka simple type theory: http://us.metamath.org/holuni/mmhol.html It's very bare-bones, but it shows it's possible.

> Certainly there is a wealth of systems available. But the ones based on type theory, such as Coq, seem to be at least as popular as the set theory based ones...

I suspect we have to ask "popular for whom?" I'd agree that type theory is at least as popular as set theory among computer tools that formalize math. But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. Type theory probably seems "natural" to people who are used to programming languages and compilers, and thus already have a daily familiarity with types (in the computer science sense).

"It's complicated" seems like an accurate summary of affairs :-).