Symbol Reference: = — Class & Term Equality Predicate (=, AST Constructor: TpEq)

= \(=\) — Class & Term Equality Predicate (=, AST Constructor: TpEq)

Binary identity predicate X = Y on classes and typed terms, governed by Left/Right ∈-Soundness (RulClassComprehension (3.01)), Extensionality (AxmExtensionality (3.10)), and Intensionality (AxmIntensionality (3.11)).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	= \(=\)
Category	Predicate Symbol (Binary Identity Relation)
SML AST Constructor	`HP (TpEq of (UCol * 'a * 'a)) [in datatype Truth_p, typetheory.ML:660]`
Constructor Arguments	1. Sort A : UCol; 2. Left term X : A; 3. Right term Y : A
Metatype / Signature	`Class × Class → Bool \| A × A → Bool`
Binder Status	No — Binary Identity Predicate Symbol
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`=`
How to Understand It	SML AST Constructor: `HP (TpEq of (UCol * 'a * 'a))` in `Truth_p` (`typetheory.ML:660`). Takes conglomerate type `A : UCol` and two operands `(X : A, Y : A)`.
Canonical Law / Usage	`(∀(z:Class)((z ∈ X) ⟷ (z ∈ Y))) → (X = Y)`
Related Symbols & Kernel Entries	Axiom AxmLeftInSound (3.08): “Membership respects equality from the left” Axiom AxmRightInSound (3.09): “Membership respects equality from the right” Axiom AxmExtensionality (3.10): “Extensionality” Theorem AxmIntensionality (3.11): “Intensionality”(admissible)