appendix sectionnotation

Identity, records, and datatype descriptions

notation	meaning	owner
notation	meaning	owner
${Id}_{A} (a, b)$ , $J (C, d, a, b, p)$	identity type and generic-endpoint eliminator	chapter 30
$IR (S)$ , $IIR (S) (i)$	inductive–recursive and indexed inductive–recursive types	chapter 31
$\vec{s} \equiv_{Δ} \vec{t}$	homogeneous equality between instantiations of a dependent telescope	chapter 31
$l \| r$ , $l . r$	Pollack restriction and rightmost named projection	chapter 79
$[[- {]]}_{CPT}$	translation from the fresh-label Pollack fragment to CPT records	chapter 79
$[[D]] (X)$ , $Mu (D)$	interpretation of a regular code and its selected fixed point	chapter 80
${refill}_{D} (u, q)$	rebuild a layer after replacing recursive positions by results	chapter 80
$ISPT (\vec{I})$ , $SPF (\vec{I}, O)$	MAG indexed strictly-positive type and family codes	chapter 80
${EqDesc}_{i} (I)$	finite regular description fragment supporting equality	chapter 80