Reverse glyph index

This index records the glyphs most likely to be confused at chapter seams. Local field-standard uses remain legitimate when declared.

glyph	admitted meanings	forbidden silent collision
glyph	admitted meanings	forbidden silent collision
$=$	meta-level equality; unambiguous object identity in a purely object-level passage	judgmental equality
$\equiv$	judgmental equality	dimension equivalence or definition
${\equiv }_{\mathcal{L}}$	computational conversion in the frozen Nuprl-style program language	judgmental equality
$:=$	definition	theorem conclusion
${\doteq }_{\mathsf{L}}$	strict equality of Timpl level expressions	object or judgmental equality
$\simeq$	equivalence	judgmental or observational equality
$\cong$	isomorphism	equivalence when structure matters
${\approx }_A$	observational equality at $A$	homotopy
${\sim }_{\mathsf{c}}$	gradual consistency	homotopy or observational equality
${⊑}_{\mathsf{ty}}$	gradual type precision	context, source, target, frame, environment, or domain approximation
${⊑}_{\mathsf{ctx}}$	gradual context precision	type, source, target, frame, environment, or domain approximation

glyph	admitted meanings	forbidden silent collision
glyph	admitted meanings	forbidden silent collision
${⊑}_{\mathsf{src}}$	gradual source-term precision	type, context, target, frame, environment, or domain approximation
${⊑}_{\mathsf{C}}$	typed target precision	type, context, source, frame, environment, or domain approximation
${⊑}_{\mathsf{F}}$	related-frame precision	type, context, source, target, environment, or domain approximation
${⊑}_{\mathsf{e}nv}$	related-substitution precision	type, context, source, target, frame, or domain approximation
${⊑}_{\mathsf{D}}$	domain approximation	gradual precision
${⇝}_0$	root contraction	elaboration
$⟶$	compatible one-step reduction; a labeled local variant when declared	elaboration
$e{\Downarrow }_{\mathsf{A}}n,e\Downarrow v$	arithmetic-fragment and full-language big-step evaluation, respectively	silent change between the two generated relations
$e{⟶}_{\beta }{e}^{\prime },A{⟶}_{\beta }B$	the shared beta-step glyph on term and constructor operands	a silent change of syntactic level
$⇝$	elaboration or insertion output	reduction
$\circ$	category composition or explicit-substitution composition, as declared	silent change of composition convention

glyph	admitted meanings	forbidden silent collision
glyph	admitted meanings	forbidden silent collision
$\Rightarrow$	sequent arrow, context-substitution arrow, or natural-transformation arrow, as declared	unannounced change of role
$[]$	postfix substitution, explicit type application, or a declared system/face form	evaluation-context plugging
$[[-]]$	semantic interpretation	syntax-to-syntax translation
$\mathrm{\Omega }$	loop-space iteration	strict proposition sort
$\mathbf{Set}$	external category of sets	internal type of small sets
$\mathsf{Set}$, ${\mathbf{Set}}_{\mathcal{U}}$	internal small-set type and its category	external metatheory
$\mathrm{\#}$, $\uplus$	disjoint resources or disjoint heaps, by declared shared abstraction	unrelated overload

In semantic statements, $A⟶B$ is an ordinary function between sets or cpos; it is neither reduction nor elaboration.