#
Homotopy Type Theory
dependent type > history (Rev #4)

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

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

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

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

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

### See also

‘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.