Homotopy Type Theory
dependent type (Rev #4)

A dependent type is a family of types indexed by - “depending on” - values of another type.

Given a type AA in a universe of types 𝒰\mathcal{U}, a dependent product type (or ‘pi-type’) BB is a family of types:

Π (a:A)B(a)\Pi_{(a:A)}B(a)

Similarly, a dependent sum type (or ‘sigma-type’) BB is a family of types:

Σ (a:A)B(a)\Sigma_{(a:A)}B(a)

See also

Dependent type’ on the nLab wiki.

category: type theory

Revision on September 4, 2018 at 13:01:08 by Ali Caglayan. See the history of this page for a list of all contributions to it.