appendix sectionnotation

Categories and categories with families

symbol	meaning	first
symbol	meaning	first
$C, C^{op}$	a category named $C$ and its opposite	chapter 52
$g \circ f, {id}_{a}$	categorical composition and the identity on $a$	chapter 52
${hom}_{C} (a, b)$	arrows from $a$ to $b$ in $C$	chapter 52
$Ctx, Rel, Mon, Cat$	named categories used as running examples	chapter 52
$[C, D], [C^{op}, Set]$	functor and presheaf categories	chapter 52
$F \Rightarrow G, Nat (F, G)$	a natural transformation and their collection	chapter 52
${Tm}_{A}, Env$	the term presheaf at $A$ and the closed-environment functor	chapter 52
$Paths, Free (G)$	reduction-path category and free category on $G$	chapter 52
$\int K, {Ctx}_{0}$	category of elements and canonically named context category	chapter 52
$e [σ]$	action of substitution $σ$ on term $e$	chapter 52
$Set$	external category of sets	chapter 52
$Fam$	external category of set-indexed families	chapter 54
$Ty, Tm$	type and term presheaves/data of a CwF	chapter 54
$y$	Yoneda embedding	chapter 52
$[[e]]$	semantic interpretation of syntax	chapter 55
$Γ . A$	context comprehension	chapter 54