title: Difference between type parameters and indices?
body: <p>I am new to dependent types and am confused about the difference between the two. It seems people usually say a type is <em>parameterized by another type</em> and <em>indexed by some value</em>. But isn't there no distinction between types and terms in a dependently typed language? Is the distinction between parameters and indices fundamental? Can you show me examples showing difference in their meanings in both programming and theorem proving?</p>