Symbol Reference: (a, b) — Ordered Class-Pair Functional Symbol ((a, b), AST Constructor: CpOPair)

(a, b) \((a, b)\) — Ordered Class-Pair Functional Symbol ((a, b), AST Constructor: CpOPair)

Binary Dunaev ordered class-pair functional symbol (A, B) = mark(A, 1) ∪ mark(B, 2) supporting arbitrary proper classes (Entry DefDunaevOrderedPair (3.76)).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	(a, b) \((a, b)\)
Category	Functional Symbol (Binary Class Operator)
SML AST Constructor	`HC (CpOPair of ('Class_EXP * 'Class_EXP)) [in datatype Class_p, typetheory.ML:565]`
Constructor Arguments	1. First component A : Class; 2. Second component B : Class
Metatype / Signature	`Class × Class → Class`
Binder Status	No — Binary Mixfix Functional Symbol (Dunaev Ordered Class-Pair (A, B))
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`(a, b)`
How to Understand It	SML AST Constructor: `HC (CpOPair of ('Class_EXP * 'Class_EXP))` in `Class_p` (`typetheory.ML:565`). Takes two class arguments `(A : Class, B : Class)`.
Canonical Law / Usage	`(A, B) = mark(A, 1) ∪ mark(B, 2)`
Related Symbols & Kernel Entries	Definition DefDunaevOrderedPair (3.76): Ordered pair(Dunaev's tagged class pair) List Tagging mark (Entry DefNaturalNumberModels (3.50)) First Projection pr1 (Entry DefDunaevOrderedPair (3.76))