Comment by nyrikki

Intuitionism And constructivism is fundamentally how computers function.

> “But if it can be stated in such a way that it is as intuitively clear as the other other axioms of set theory, then it will likely be accepted"

The internal/external logic of sets is exactly where Set gets confusing with computation.

Subsingletons (mere props) being choice theoretic is exactly where we have to resort to HoTT etc..

That shift in limitations from internal vs. external is a lens on many independence results.