1
$\begingroup$

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are instantiated with proper values at the time of type checking. I am wondering, what is the importance of this? Looking at the rules it seems like I could just as well have not specified the indexes and for the user nothing would ever be any different.

So what difference would the user see if I simply had the rules $Type : Type$ and $\frac{E[Γ] ⊢ T : Type \,\,\,\, E[Γ::(x:T)] ⊢ U : Type}{E[Γ] ⊢ ∀ x:T,U : Type}$ in place of the rules that talk about the indexes?

$\endgroup$