Skip to main content
Proof Assistants Beta

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

16
  • $\begingroup$ Thank you very much. Can you provide a precise reference for CIC, that lists all the rules in one place precisely? I am not comfortable with the references I can find, which mix precise type-theory syntax with a lot of verbose English phrases. In particular, it seems that the CIC in your post is actually not the same as the CIC in the introduction I cited... $\endgroup$
    – user21820
    Commented Mar 30, 2022 at 12:56
  • $\begingroup$ Like MLTT, CIC is used for several closely related systems — they all feature dependent types, an impredicative universe and inductive types, but there is some fuzziness surrounding the specifics of the (co)inductive types and the predicative universes (polymorphism, cumulativity...). I think my use of the word roughly matches the introduction of C. Paulin-Mohring, though. $\endgroup$
    – Loïc Pujet
    Commented Mar 30, 2022 at 15:07
  • $\begingroup$ No, the one in my cited PDF is impredicative, but the one in your post seems to be predicative, because you talk later about adding impredicative universes. If there is fuzziness everywhere in the literature, can you please list out explicitly all the rules in the CIC that your post is supposedly about? Thanks! $\endgroup$
    – user21820
    Commented Mar 30, 2022 at 15:12
  • $\begingroup$ Other than that, there is a description in the Coq reference manual (with all the options, including SProp, coinduction, and several notions of polymorphism — but the complexity of this version means that its meta-theory is not completely clear), in Timany and Sozeau's "Consistency of the pCuIC" (but this system does not have any kind of inductive types inside of Prop, which means there is much less functions on the inductive natural numbers), and in the various formalizations of the system, such as MetaCoq. $\endgroup$
    – Loïc Pujet
    Commented Mar 30, 2022 at 15:13
  • $\begingroup$ Maybe I was not clear enough in my answer: MLTT is predicative, and the CIC is impredicative (I describe it as an extension of CCω, which is impredicative, with inductive types). I don't believe I mention CIC before talking about impredicativity, so it would help me if you could point out what made you think that. $\endgroup$
    – Loïc Pujet
    Commented Mar 30, 2022 at 15:16