Σ \(\Sigma\) — Dependent Sum Type Binder (Σ, Entry DefSigmaModel (3.38))
Dependent sum / disjoint union constructor Σ(B) consisting of all Dunaev pairs (x, y) with x ∈ Dom(B) and y ∈ B(x).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
Σ
\(\Sigma\)
|
| Category | Binder / Type Constructor (Dependent Sum) |
| SML AST Constructor | Sigma_def_entry [Defined Class/Type Constructor, foundations.ML / entries.ML:DefSigmaModel (3.38)] |
| Constructor Arguments | 1. Set-and-class-valued family B : Family (or bound variable a : A and family B(a)) |
| Metatype / Signature | (F : Family) → Class | (x : A) × B(x) → Type |
| Binder Status | YES — Dependent Sum Binder / Conglomerate Type Constructor |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \Sigma |
| How to Understand It | SML AST Constructor: Defined class/type binder in Entry DefSigmaModel (3.38) ( |
| Canonical Law / Usage | ((x,y) ∈ Σ(B)) ⟷ ((x ∈ Dom(B)) ∧ (y ∈ B(x))) |
| Related Symbols & Kernel Entries |