Showing changes from revision #4 to #5:
Added | Removed | Changed
A dependent < 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.