The original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.) In the

The original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.) In the Idris2 github repository, Guillaume Allais goes a step further and shows a well-named version. There the types of terms and values are indexed by the list of names in the environment and the compiler checks that the manipulation of deBruin levels and indices is correct: https://github.com/idris-lang/Idris2/blob/main/libs/papers/Language/IntrinsicScoping/TypeTheory.idr https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...