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.
Revision on September 4, 2018 at 17:01:08 by Ali Caglayan. See the history of this page for a list of all contributions to it.