So I came across dependent typing at Scala Exchange (at this talk), and the speaker went through an example where he indexed a vector using Peano numbers and used it to encode properties about operations on vector in the types of those operations - I've also seen this a few other places since as well. I read more about dependent types on Wikipedia, but I couldn't quite translate the example above into sigma/pi dependent type distinction.
So, my question is: are the types being used in the Peano-indexed vector sigma or pi dependent types? Also, could someone please provide or point me to an example of the kind that they're not so I have a examples of both? (preferably in Scala)