appendix sectionnotation

Pure type systems

symbol	meaning	first
symbol	meaning	first
$*, ◻$	type and kind classifiers in the lambda-cube instances	chapter 22
$S = (S, A, R)$	sorts, axioms, and product triples of a PTS	definition 60.2
$Γ ⊢_{S} M : A$	typing under the specification $S$	definition 60.3
$M =_{β} N$	equivalence generated by compatible beta-reduction	definition 60.2
$r_{\to}, r_{2}, r_{ω}, r_{P}$	ordinary, polymorphic, operator, and dependent product triples	equation 60.1
$λ_{I}$	lambda-cube vertex selected by optional axes $I$	definition 60.5