Showing changes from revision #2 to #3:
Added | Removed | Changed
A dependent type is a family of types indexed by - “depending on” - values of another type.
Given a type in a universe of types , a dependent product type (or ‘pi-type’) is a family of types:
Similarly, a dependent sum type (or ‘sigma-type’) is a family of types:
‘Dependent type’ on the nLab wiki.