appendix sectionnotation

Dependent and computed-equality distinctions

form	semantic role	owner / collision
form	semantic role	owner / collision
$T_{0}$	full intensional base of Chapters 70–74	chapter 26; never the normalization fragment
$T_{Π 2}$	structural, dependent-product, and Boolean normalization fragment	convention 49.8; not $T_{0}$
$T_{H}$	universe-free Hofmann core used for the ETT inhabitation comparison	definition 35.26; not $T_{0}$
${Id}_{A} (a, b)$	intensional identity type	chapter 30; not observational equality or cubical path
$a \approx_{A} b$	observational equality code at $A$	chapter 79; not homotopy
${PathP}_{i . A} (a, b)$	cubical path in a line of types	chapter 80; dimension binder $i$
$Γ ⊢ φ true$	proof-irrelevant cofibration truth	chapter 81; not an inhabited object type
${coe}_{i . A}^{r \to s} (a)$	Cartesian coercion in the line $i . A$	definition 81.7; source and target are explicit