Comment by logicchains

Since this seems to support inductive types, would it be correct to say that it's based on the calculus of inductive constructions (CIC), not the plain CoC? Basing a dependently-typed language on pure CoC (plus some other features weaker than inductive types; it's been proven impossible in CoC alone) is an open research problem (see e.g. Cedille and Formality).