appendix sectionnotation

Scoped operations and explicit substitution

symbol	meaning	first
symbol	meaning	first
$Σ, Γ$	ordinary-operation and scoped-operation signature functors	23.1
$P_{o}, R_{o}$	ordinary parameter and response sets for operation $o$	23.1
$P_{s}, Q_{s}$	ordinary parameter and scoped-position sets for scope creator $s$	23.1
$T_{Σ, Γ} A$ (usually $T A$ )	scoped syntax with return set $A$	23.2
$Var, Op, Scope$	return, ordinary operation, and scoped-operation constructors	23.2
${Scope}_{s} (p; X; m; k)$	elementwise scoped node: parameters, intermediate result set, scoped computations, and outside continuation	23.2
$[X, m, k]$	reindexing class of an elementwise scope representative	23.4
$t [f]$	explicit substitution of $f : A \to T B$ for return leaves of $t : T A$	23.9
$≫ =$	scoped-syntax bind, defined by explicit substitution	23.12