>>13053833Sir, you're a retard. CT is typically described in a meta-theory that *is* classical and enjoys copious amounts of choice. Contrarily by what is claimed by
>>13053758, CT is not a foundation. Rather it's a set of patterns that can be used to classify things in a foundation that needs to be quite set-theoretical. CT is what you get when you give LSD to Bourbakists, a gang famously known to have been filtered by logic. (See e.g. "Hilbert, Bourbaki and the scorning of logic" on that topic.)
The fact that the object theories CT describes can be intuitionistic, or linear, or whatever, only reflects the fact that CT is precisely that, a syntax for object theories. You can perfectly describe topoi in a set-theoretical world. Worse, that's actually the way it is traditionally done, i.e. in terms of subobjects, that is sets. You can't do shit in topoi without meta-unique-choice for instance, and don't get me started on sheaves.
