appendix sectionnotation

Proof production, levels, casts, and generated action

notation	meaning	owner
notation	meaning	owner
$Rw (Γ; R; t; u; v)$ , ${reflex}_{R}$	certified contextual rewrite with witness $v$ , and the supplied reflexivity witness for $R$	chapter 115
$a_{β}^{ω}$ , $a^{S} [o; src (ω)]$ , $a^{S} [o; new (o_{t})]$ , $Γ ⊢_{n} e : A$	raw reference with lexical target; expanded copied or constructed reference with scope set and resolved origin; phase-indexed typing	chapter 116
$Level$ , $Below (t, u)$ , $N (t)$	first-class level type, join-induced level order, and finite-map level normal form	chapter 117
$elim (I, s) allowed$ , $L (Θ)$	permitted inductive elimination and sort-erased prenex context	chapter 118
$Coe (A, B)$ , ${prog}_{p}$	generated coercion paths and the target cast program denoted by a path	chapter 119
${map}_{F}$ , $f {\circ_{F}}_{F} g$ , $[[D {]]}_{X}$	generated type-former action, its domain composition, and interpretation of a positive description	chapter 120