#
Homotopy Type Theory
dependent type > history (changes)

Showing changes from revision #4 to #5:
Added | ~~Removed~~ | ~~Chan~~ged

~~ A~~ ~~ dependent~~ < 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.

~~
~~
Last revised on June 9, 2022 at 20:44:18.
See the history of this page for a list of all contributions to it.