Pi type (dependent product)

Layer 0 — Mathematicsin the Type Theory subtree

Generalizes function-type to Pi(x:A) B(x) where output type may depend on input value; unifies forall-quantifier and dependent function; basic constructor in MLTT.