Basic idea of using singleton types like Nat n where n is a value from the index domain, to connect program expressions and index expressions.  The data value of type Nat n is a copy of n, but living in the syntactic category of program expressions.  This allows programs to operate on a proxy for n.  Singletons library in Haskell mentioned.