If "every intuition from set theory goes against [CoC]", and "slight modifications will jinx the consistency", why should we accept such a weird system? How do we even know it is consistent to begin with?

@user21820 Yes, and it is exactly my belief that we shouldn't accept such a system!

Hold on, can I confirm that you believe that we should not accept CoC because it is impredicative? This is the first time I see someone on SE who is as familiar with CoC as you and who seems to reject it on grounds of impredicativity, so I'm kind of surprised. Do you also reject full ZFC (where unbounded specification and replacement are also impredicative)? Thanks for your reply!

@user21820 I'm not against impredicativity in general. And propositional inpredicativity is just fine. But CoC is impredicative ay both levels. As a side note: Coq does not use CoC.

Oh. But I recall reading that CoC has a model in ZFC, and in fact CoC plus universes, which I also thought is the underlying type theory for Coq. If one believes ZFC is meaningful for any reason, then it must translate to a belief that CoC is meaningful as well. So now I'm not really sure how CoC is any worse than full ZFC. Am I missing something?

@user21820 Having translations does not prove any sort of "equi-meaningfulness". Also, if you extend CoC with one more universe, and (just as CoC does) allow the function spaces to reside in the same sort as its codomain, then you have Girard's paradox. Coq does not have impredicative Set (without any flags).

@Trebor Thanks for giving a gist, though I am unfortunately not sufficiently familiar with CoC to understand your comment. Can you give a short but more technical explanation of what you think is the problem with CoC in principle? I understand that it is difficult to talk about what you don't believe is meaningful, but is it possible to pinpoint a specific aspect or ideology behind CoC that is problematic in your view?

I think the essential thing here is that what is psychologically (which means it is not respected by translations) regarded as sets is impredicative. So you get $X \cong P(P(X))$ even for sets $X$.

Coq however, has given up on this, so only what is regarded as propositions can be impredicative. (The --impredicative-set option reenables it)

I work in Agda on a routine basis, which does not have any sort of impredicativity. Even propositions are stratified. (Not unless you combine weird flags and options, of course)

@Trebor: Hello! And thanks for your time! I would like to know what you mean by psychologically having X ≅ P(P(X)) for set X, and how it relates to having "one more universe". Is there a problem if we just have CoC with ω-many universes? I thought they were stratified.

@Trebor And sorry for a tangential question about Agda: I learnt that sized types yields inconsistency and so was marked as unsafe. Are sized types included in your routine work in Agda? If so, what is your resolution? If not, why do you think people put it into Agda in the first place?

Sorry for barging into your conversation :P, but another reason to be against CoC is that (IMO) we almost never really need full impredicativity unless you are proving the consistency of system F. So it seems like a lot of extra headaches for very little use. But to be fair (I may be completely wrong), I imagine Coq uses impredicativity to deal with program extraction in a principled way.