Sigma type (dependent sum)

Layer 0 — Mathematicsin the Type Theory subtree

Generalizes pair-type to Sigma(x:A) B(x); unifies exists-quantifier and dependent record; first-projection extracts witness, second-projection extracts proof.