By foundations here, I didnt mean foundations of mathematics, rather the amount of material a student needs to read to become familiar with the basic definitions of what a space means. We can teach topology to undergrads, can we teach higher categorical notions of space? Even schemes themselves had a daunting reputation some time back, now we have derived stacks which involve infinite categories.
> You can just pick up Higher Topos Theory and start reading
Yes, but my point, as illustrated in SDG example, was that definitions can be easy or hard depending on which foundations you use. You havent mentioned whether you disagree with this and if you see Kock's book, I think you will agree.
When dealing with higher categories, a foundations which uses '=' symbol in a different way, with an equivalence relation(modelled on homotopy equivalence) playing a much more prominent role could make the theory much more natural.
Note, that I am not even emphasizing sets vs type theory here, but excluded middle and a good notion of equivalence(and equivalence between equivalences... like in homotopy theory) in the foundations.
Maybe a lot of this debate will get dissolved if we just use two different words for 'examining consistency of axioms' and 'naturality of theory as encoded in a given system' instead of using the same word - foundations - for both of them.
At the very least if discussions begin with an awareness of this distinct usage, there would be lot less talking past each other.
Urs Schreiber makes the same point about naturality here - https://golem.ph.utexas.edu/category/2016/03/foundations_of_...