Symbol Reference: fst — Dependent Pair First Projection Functional Symbol (fst, Entry DefSigmaModel (3.38))

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

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

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	fst \(\mathrm{fst}\)
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	`Σ(x:A), B(x) → A`
Binder Status	See Category & Signature above
Defining Kernel Entries (ML Labels)	See Related Symbols & Kernel Entries below.
LaTeX Form	`\mathrm{fst}`
How to Understand It	SML AST Constructor: Projection on dependent sum `Σ` (Entry DefSigmaModel (3.38)) and Dunaev class-pair `pr1` (Entry DefDunaevOrderedPair (3.76)).
Canonical Law / Usage	`fst((a, b)) = a`
Related Symbols & Kernel Entries	Dependent Sum Σ (Entry DefSigmaModel (3.38)) Class-Pair First Projection pr1 (Entry DefDunaevOrderedPair (3.76))