1
$\begingroup$

This question already has an answer here:

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$

marked as duplicate by Gilles Mar 25 '15 at 21:50

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.