Foundations of Math: Sets vs Categories vs HoTT

There's been a controversy lately about the foundations of mathematics. It was controversial when it first was discovered in the late 19th/early 20th century when the foundations were being developed, controversial mostly because most mathematicians didn't feel its necessity and also because as a young field things just hadn't been resolved. But some of the greats (Hilbert, logicians) thought foundations were needed.

The development of foundations started almost entirely with logicians and philosophers (Boole, Cantor, Peirce, Frege, Zermelo, Russell) creating the axioms of set theory all based on the concept of set membership. This was not particularly in the center of mathematical development. It was essentially completed in the 1920's, then controversialized by Gödel in the 1930's, but was refined by him and other logicians (Church, Tarski, Putnam,) and set theorists over the next 30 years.

Then in the 60s, an alternative foundations was proposed and that was category theory all based non the concept of maps betwen objects (morphisms) representing similarity. It felt like category theory could model most any mathematical field that way, even if objects and morphisms were not central, and the diagrams it created seemed to show similarities among the disparate fields of math. Category theory itself was created in the 40s by MacLane and Eilenberg but Lawvere began in the 60s to think of it additionally as an alternative foundations.

More recently, the 2000's, higher order type theory (HoTT) has been proposed and developed as an alternative foundations (mostly by Voevodsky). I don't know much about HoTT other than it seems like a subset of Category Theory.

Without going into the details of each of these foundations, it seems to me, as a semi-educated outside who knows these fields very superficially, that the word 'foundations' means something different to these different alternatives.

For set theory, it is a foundation for reasoning, for specifying proofs, for how you can justify things. For the others, the foundation is for content and similarity among branches of mathematics, what is known in mathematics. That is, these aren't really exclusive foundations, they both have their purposes and they are non-conflicting they're just different kinds of formalisms rather than competing for the same ideas. It is also an intra-mathematical result that they are interpretable in each other; the concepts in one are translatable to concepts in the other. You can do HoTT with set theory as the underlying basis and similarly you can do set theory with elements defined in terms of HoTT.

My preference is for set theory. Another reflection on this is that set theory and axiomatics is easy to explain early (to those with less mathematical maturity) using very basic mathematical analogies, and category theory and HoTT is more difficult needing lots of higher math to understand and use as non-trivial examples. Also, set theory includes logic (somehow, I'm not sure if is as additional machinery or if it is considered a consequence of set theory), and I don't know what kind of inference mechanism is allowed with HoTT or category theory.

Of course this is entirely biased of me because I think that Turing Machines form the best foundation because it is very simple to understand and is entirely operational, and is a metaphor for all computation which is all that mathematics is good for anyway!