Comment by vintermann

> Calculus of inductive constructions (Coq, Lean): the original paper (describing a weaker system) begins “The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style,” and the paper makes no foundational claims. Coquand’s retrospective paper makes no such claims either. Since it turns out to be significantly stronger than ZF set theory,

Whoa, whoa, hold your horses here. Why didn't THAT claim come with an explanatory hyperlink?