𝒱 / V \(\mathcal{V}\) — Universal Class of All Sets (𝒱, AST Constructor: CpSets)
0-ary class constant 𝒱 = {x | ⊤} denoting the proper class of all sets (Entry DefUniversalClass (3.05)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
𝒱 / V
\(\mathcal{V}\)
|
| Category | Functional Symbol (0-ary Class Constant) |
| SML AST Constructor | HC CpSets [in datatype Class_p, typetheory.ML:556] |
| Constructor Arguments | 0-ary constant (no arguments) |
| Metatype / Signature | Class |
| Binder Status | No — Defined 0-ary Functional Symbol (Universal Class of All Sets) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \mathcal{V} |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | 𝒱 = {x | ⊤} |
| Related Symbols & Kernel Entries |