Comment by zarzavat
2 years ago
The calculus of inductive constructions is not very big? It seems simpler than ZFC to me. The version that Coq uses is quite large, but that's the difference between theory and practice: Coq is designed to be maximally usable not minimally simple.
Well, inductive constructions need positivity conditions to be consistent. These are complicated enough to suggest that they need to be proven instead of accepted as part of the formal system.