Π \(\Pi\) — Dependent Product Type Binder (Π, Entry DefSigmaModel (3.38))
Dependent product constructor Π(B) consisting of all families f with Dom(f) = Dom(B) and ∀(x∈Dom(B))(f(x) ∈ B(x)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
Π
\(\Pi\)
|
| Category | Binder / Type Constructor (Dependent Product) |
| SML AST Constructor | Pi_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 Product Binder / Conglomerate Type Constructor |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \Pi |
| How to Understand It | SML AST Constructor: Defined class/type binder in Entry DefSigmaModel (3.38) ( |
| Canonical Law / Usage | (f ∈ Π(B)) ⟷ ((f is a family) ∧ (Dom(f)=Dom(B)) ∧ ∀(x∈Dom(B))(f(x)∈B(x))) |
| Related Symbols & Kernel Entries |