appendix sectionnotation

Logic-enriched and erased same-subject notation

notation	meaning	owner
notation	meaning	owner
$Γ; Δ ⊢ P$ , $p prop$ , $V (p)$	LTT entailment, small-proposition code, and decoding	chapter 92
$Set (T (a))$ , ${x : T (a) ∣ p}$	predicative set type and small comprehension	chapter 92
$x : A \cap B (x)$ , $both$ , $left$ , $right$	same-subject dependent intersection and its typed views	chapter 37
$ι x . T$ , $selfGen$ , $selfInst$	System S subject-dependent self type and typing views	chapter 94
${f ∣ x : A \to B [f, x]}$ , $f ↾ A_{< a}$	very-dependent function and predecessor restriction	chapter 95
$Λ x . t$ , $t - u$ , $[t, u]$ , $t .1$ , $t .2$	erased abstraction/application and CDLE intersection views	chapter 38
${t ≃ u}$ , $β {u}$ , $ρ p$ , $ϕ p$ , $δ - p$	CDLE heterogeneous equality, proof, rewrite, direct computation, and separation	chapter 38
$Cast (A, B)$ , $TpEq (A, B)$ , $Rec (F)$	identity-erasing cast, two-way cast equivalence, and derived monotone recursive type	chapter 38