1. ZFC is fairly "obvious" when taught the right way. Unfortunately, most people do have not the privilege of a good set theory instructor.
2. Whether V equals Ultimate L, for example. There's "pop math" coverage available [1], as well as more technical introductions by Woodin if you Google for them.
3. I'm not sure what reasons you're referring to; can you enlighten me? I can guess, but the ones I'm guessing are not very good, and I'd rather not attribute weak arguments to you or them.
4. The Stacks Project, for one [2]. It covers most of the foundations of modern algebraic geometry, is of extremely high quality, and is regularly cited in research papers.
[1]: https://www.quantamagazine.org/to-settle-infinity-question-a...
3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic correspond exactly to the types of types programs in certain models of programming languages, and the proofs of intuitionistic logic to well-typed programs in those models. This is called the Curry-Howard isomorphism, and has been a very fruitful source of inspiration for type theory. For example, it was originally noted for intuitionistic propositional logic only, but adding universal quantification gives a type theory with so-called parametric polymorphism, which was later developed into generics in Java and other languages. I have seen modal logic used to model distributed computation, and linear logic inspired work which eventually led to Rust's borrow checker.
2. What are these "substantive problems"? I don't have any experience in foundations, so I'm genuinely curious.
3. Sure, intuitionistic mathematics has very little popularity, but a lot of that popularity is among computer scientists, for fairly obvious reasons.
4. The HoTT book and the nLab are two of the most out-in-the-open developments in math I've seen --- the HoTT book was even written in a public GitHub repo iirc. Naturally that has a lot of appeal for HN. If you have anything similar (blogs, wikis, etc.) for mainstream foundations, I'd love to read them.
5. Yeah, personally, I'm not really convinced that HoTT is a good idea, but I guess we'll just have to wait and see.