Use this tag for questions about dependent types, which are families of types which vary over elements of another type.

References:

nLab
Wikipedia