So far I am aware of UniMath/HoTT, which are both pretty vast Coq collections of "foundations of mathematics" theorems, lemmas, and proofs. I don't know how "complete" these can be considered, as I don't know if there are any books or sources describing all of the features that need to be accounted for in mathematics to have a "complete foundation". Maybe you could shed light on if there are any references to such systems which list all of the features required to encapsulate "all" of fundamental math.
I have also recently been shown the Isabelle Archive of Formal Proofs. This seems to be just as vast as UniMath or HoTT on the surface, but I am no expert.
Are there any other such projects that have compiled the foundation of mathematics into a formally verified codebase like these 3 projects have done? What is the most complete or "best" one?
I doubt that a succinct unbiased answer can be given, so I'll try to give a broad overview of what's out there instead.
Basically, there are a number of different approaches to logic and foundations in general, but for the vast majority of everyday mathematical statements/purposes, most are suitable. So it's hard to say which ones are "more complete" than others, if they all can do the job. For examples of getting into the weeds about differences across theorem provers, see Proof strength of Calculus of (Inductive) Constructions on MO or Importing (translating) Mizar into Coq (Axiomatic set theory into constructive type theory) here on MathSE.
Depending on where exactly you draw the line, some proportion of the theorem checkers and similar on Freek Wiedijk's list are up to the task of verifying an approach to foundations. Currently, he lists 44 "first order provers", 38 "proof checkers", 26 "tactic provers", and 43 "theorem provers", where his definitions of these categories are given on this explanation page. I don't honestly know what proportion of these have a publicly available foundation for math. And as you noted, some (like Coq) have multiple.
Since you ask about the "best" one, a proxy might be to measure how many notable theorems have been verified with a given system (though in a case like Coq, different theorems might have been on top of different foundations). Wiedijk has a list of 100 notable theorems and which have been verified in major systems, where major means they have verified many of the theorems or a theorem not covered by the others. At the time of writing, the major contenders are HOL Light, Isabelle, Metamath, Coq, Mizar, Lean, and ProofPower.
All of those major systems have a variety of different approaches to foundations, representing theorems/proofs, verifying theorems, etc. The goals of a project like the Metamath Proof Explorer are very different than the goals of, say, most people trying to verify things with Coq.