  In order to avoid well-know paradoxes associated with self-referential
definitions, higher-order dependent type theories stratify the theory using a
countably infinite hierarchy of universes (also known as sorts), Type$_0$ :
Type$_1$ : $\cdots$ . Such type systems are called cumulative if for any type
$A$ we have that $A$ : Type$_{i}$ implies $A$ : Type$_{i+1}$. The predicative
calculus of inductive constructions (pCIC) which forms the basis of the Coq
proof assistant, is one such system.
  In this paper we present and establish the soundness of the predicative
calculus of cumulative inductive constructions (pCuIC) which extends the
cumulativity relation to inductive types.
