Comment by dwheeler

I would have expected to see at least more of a discussion about Metamath.

Metamath by itself does not pick any particular foundation. It just lets you state axioms, then prove theorems from axioms and other proven theorems (letting you stack them up). So you can choose your axioms. Set theory with classical logic? Or with intuitionistic logic? Maybe you'd prefer simple type theory? Carry on!

That said, the largest Metamath database (set of axioms and proven theorems) is the "Metamath Proof Explorer". It's based on ZFC set theory with classical logic. It turns out that ZFC set theory is quite enough to model structures. This database does add the Tarski–Grothendieck Axiom for certain uses of category theory (the same axiom added by Mizar), but it's only used when it's needed and that is quite rare. Heck, even the axiom of choice turns out to be unneeded in many cases. You certainly don't have to use ZFC with classical logic as your fundamental starting point (indeed, someone who rejected classical logic would not accept it). But you can go a long way with it.

More information about Metamath is here: https://us.metamath.org/

More information about the Metamath Proof Explorer database (based on ZFC + classical logic) is here: https://us.metamath.org/mpeuni/mmset.html