Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent? This answer says,

IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles — see Benjamin Werner's "Sets in types, types in sets". (This is because of the presence of a universe hierarchy in the CIC.)

But, I read "Sets in types, types in sets" and discovered that the book does not prove this statement. It only conjectures the strength of CIC.
Has "CIC and ZFC + countably many inaccessible cardinals are equiconsistent" been proven or disproven?
 A: The situation is a bit subtle. One can interpret CIC in any model of ZFC with infinitely many inacessibles. However, interpreting ZFC in CIC is more subtle. First one needs to assume the law of excluded middle and choice in CIC (and perhaps quotient types depending on how smooth we want things to work). These are very strong assumptions and they increase the consistency strength over plain CIC, which appears to be much weaker.
Once excluded middle and choice are assumed, within each universe level $\mathcal{U}_1,\mathcal{U}_2,\ldots$ of CIC we can construct a model of ZFC. This constructs a chain $V_1 \subseteq V_2 \subseteq \cdots$ of models of ZFC where each is an end extension of the previous, up to canonical isomorphism. Thus, $V_2$ has at least one inaccessible, $V_3$ has at least two inaccessibles, and so on. Thus CIC with choice proves the consistency of ZFC + there are $k$ inaccessibles for any standard $k$. Note that I've been careful not to associate universe levels with natural numbers. Indeed, models of CIC and ZFC can have nonstandard natural numbers. However, universe levels are syntactic objects and therefore always standard.
So, the consistency of CIC with choice and excluded middle implies the $\Pi_1$ statement $$\forall k\,\operatorname{Con}(ZFC + k\text{-many inaccessibles})\tag{*}.$$
This is strictly weaker than the consistency of ZFC with infinitely many inaccessibles. However, $(*)$ is actually enough to construct a full model of CIC! By compactness, we can construct a model $V$ of ZFC with $k$ inaccessibles, where $k$ is nonstandard. In this model, we can list the first standardly many inaccessibles as $\kappa_1 < \kappa_2 < \cdots$. This hierarchy allows us to construct a corresponding sequence of universes for a model of CIC. Note that this is not an interpretation per se since we can only witness externally that $k$ is nonstandard.
Nevertheless, from the above it follows that the consistency strength of CIC with excluded middle and choice is exactly $(*)$ and therefore strictly weaker than ZFC with infinitely many inaccessibles.
A: I think "Une Théorie des Constructions Inductives" (Benjamin Werner) implies that "CIC and ZFC + countably many inaccessible cardinals are equiconsistent" is wrong. The paper proves the consistency of CIC on ZFC + countably many inaccessible cardinals.
