Mistake is often made that ZFC is the be-all and end-allultimate foundation of mathematics. Unfortunately, 1st-order ZFC (often referred to as just "ZFC") is a very weak theory.
For example, if O is the type of the ordinals, then
O
Boolean // type of all functions from ordinals into type Boolean
cannot be represented in ZFC because it does not exist in the cumulative hierarchy of sets.
No, I mean, why me, specifically? Did I accidentally say something to give the impression I find your odd rantings interesting? Because if I did, please let me know so I can correct the misunderstanding.
For example, if O is the type of the ordinals, then
cannot be represented in ZFC because it does not exist in the cumulative hierarchy of sets.