appendix sectionnotation

Higher kinds, packages, and elaboration

symbol	meaning	first
symbol	meaning	first
$κ, Ty$	kinds and the kind of ordinary types	chapter 9
$Δ ⊢ A :: κ$	constructor $A$ has kind $κ$	chapter 9
$Δ ⊢ A \equiv B :: κ$	constructor beta equality at a kind	chapter 9
$A ⟶_{β} B$	one compatible constructor-beta step	chapter 9
$A ⟶_{β}^{*} B$	reflexive–transitive constructor-beta reduction	chapter 9
${Some}_{κ} (u . A)$	Church encoding of an existential package	chapter 10
${Rel}_{κ} (C_{0}, C_{1})$	relational objects at kind $κ$	chapter 10
$\hat{A}, \hat{e}$	typed constructor and term representations	chapter 17