appendix sectionnotation

Kernel and normalization semantics

notation	meaning	owner
notation	meaning	owner
${Sing}_{A} (a)$	singleton type with distinguished element $a : A$	chapter 48
$Γ ⊢ e \Leftarrow type ⇝ A$	presyntax $e$ elaborates to the core type $A$	chapter 48
$Γ ⊢ e \Leftarrow A ⇝ a$	checking-mode elaboration of $e$ at input type $A$	chapter 48
$Γ ⊢ e \Rightarrow A ⇝ a$	synthesis-mode elaboration of $e$ , returning $A$ and $a$	chapter 48
$Γ ⊢ A \Leftrightarrow B type$	algorithmic conversion of types $A$ and $B$	chapter 48
$Γ ⊢ a \Leftrightarrow b : A$	algorithmic conversion of terms $a, b : A$	chapter 48
$[[e {]]}_{C}$	interpretation of a dependent-checker expression in Coquand’s semantic model	chapter 48
$A ⪯_{Σ, Γ} B$	conversion-or-cumulativity comparison between an inferred PCUIC type and its declarative target	chapter 48
$RawTm$	raw terms equipped separately with typing derivations	chapter 49
$Δ ⊵ Γ$	the context $Δ$ extends $Γ$	chapter 49
$Δ ⊩ a \sim d : A$	Kripke computability of $a$ with semantic value $d$	chapter 49
$nf (a)$	canonical normal form computed from a typed term	chapter 49
$Γ ⊢ u ne A$	typed neutral-form judgment	chapter 49
$Γ ⊢ v nf A$	typed normal-form judgment	chapter 49
$↑_{A} (k)$	NbE reflection of a neutral into semantic evidence	chapter 49
$↓_{A}^{n} (d)$	NbE reification of semantic evidence into a normal form	chapter 49
$reflect$	proof-relevant reflection operation	chapter 49
$reify$	proof-relevant reification operation	chapter 49
$χ @ \vec{d} ⇓ e$	least evaluation graph for applying a normalization-domain closure to semantic arguments	chapter 49
$K_{Ψ}$	readback-defined field of the world-indexed neutral partial equivalence relation at support $Ψ$	chapter 49