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 ### '[[nlab:dependent type|Dependent type]]' on the nLab wiki. category: type theory