Symbol Reference: snd — Dependent Pair Second Projection Functional Symbol (snd, Entry DefSigmaModel (3.38))

snd \(\mathrm{snd}\) — Dependent Pair Second Projection Functional Symbol (snd, Entry DefSigmaModel (3.38))

Second projection functional symbol snd(p) for dependent pairs in Σ(x:A), B(x).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	snd \(\mathrm{snd}\)
Category	Functional Symbol (Unary Projection Operator)
SML AST Constructor	`Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)`
Constructor Arguments	Typed arguments as specified by the Signature / Sort field above
Metatype / Signature	`p : Σ(x:A), B(x) → B(fst(p))`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathrm{snd}`
How to Understand It	SML AST Constructor: Projection on dependent sum `Σ` (Entry DefSigmaModel (3.38)) and Dunaev class-pair `pr2` (Entry ThmDunaevFirstProjection (3.77)).
Canonical Law / Usage	`snd((a, b)) = b`
Related Symbols & Kernel Entries	Dependent Sum Σ (Entry DefSigmaModel (3.38)) Class-Pair Second Projection pr2 (Entry ThmDunaevFirstProjection (3.77))