pCICとは
ちょっと基本的なところから行こう。
pCICと書いているが、まあ多くの人はそんなもの知るまい。
ちなみに、Coqについてそれなりの知識を持っていることを前提に話をするので、せめて利用者としての経験を要求する。
pCICはpredicative Calculus of Inductive Constructionの略称。
pがつかないCICをある。これはCoqがバージョン7まで使っていた計算。
差はSetというソートがpredicativeになったこと。*1
predicativeかimpredicativeかの差はここ（Coqのドキュメントへ）にある。
簡単に説明すると、全称限量の型が（量化されている変数の型によらず）結果の型だけで決まる場合（Setに属する型が結果なら全称限量全体がSetになる）impredicative、そうでなくて量化されている変数に依存する場合はpredicative。
今はpredicativeなので、forall x : Type, natなどとするとSetではなくTypeになる（逆に言うと、CICではSetになる）。
今日はこの説明だけにしておこうかな。
ちなみに、変な言い方だけれどもpCICと正確に書かない場合もある。
というのも、(p)CICはCoqくらいしか使わないので（少なくとも利用しているシステムで最も有名なものはCoqなので）、CIC＝Coqが使っているシステム、くらいに考えている人が多いため。
別に文句はないけど、希に見るので驚かないように。
