[random3]

Can you elaborate what's ironic (what is "this" - higher CT)?

A note on the motivations - CT was not originally intended as a foundations. This is clear from both the name (General Theory of Natural Equivalences) and construction (based on set theory, which is was and still is the foundation for most of mathematics). There was indeed work in the foundational direction and there are relevant aspects, but I don't think that's even today the core aspect of it.

[ak_111]

Yes I should point out that I am a noob in this area, so you might be right in calling me out. My understanding is that CT was invented in part to provide a robust foundation for algebraic geometry, so it is quite ironic that people are now involved in trying to rework the foundation of the foundation.

[anon291]

Not really. For many years mathematics rested on traditional first order logic and traditional naive set theory. That was revisited at the begining of the twentieth century.