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.
Last revised on June 9, 2022 at 20:44:18. See the history of this page for a list of all contributions to it.