Greetings.

Can anyone give me a link to a proof of strongly or weakly normalization of Calculus of Inductive Constructions (CIC) and a proof of consistency strength of CIC?

I use the word “CIC” as the system presented in “Inductively defined types” by Coquand, Paulin in 1990.

Similar questions are at https://coq-club.inria.narkive.com/jHBce3xb/proof-on-strong-normalization-of-cic

https://mathoverflow.net/questions/69229/proof-strength-of-calculus-of-inductive-constructions

and

https://mathoverflow.net/questions/59520/how-true-are-theorems-proved-by-coq

According to them, Werner proved strong normalization of “λP2 + Inductive Types” in 1994. Altenkirch proved but did not cover general inductive types. Werner proved the upper bound of consistency strength of CIC is ZFC+ω inaccessible cardinals in 1997. Miquel proved the lower bound is Z + ω Zermelo universes.

Is there a proof on strongly or weakly normalization of Coquand’s CIC? Are there tighter bounds of its consistency strength?

Thanks for any hint.

Regards

Kaede