EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very strict compiler.

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.

Also, this means if you are counting lines you need to include the formalisation of the logic and the axioms of ZFC inside metamath. The kernel of Coq is similarly a quite short program.

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 (For instance the first formalised proof of the four colour theorem and Gödel’s theorems were in Coq).