appendix sectionnotation

Universes

symbol	meaning	first
symbol	meaning	first
$U_{i}$	universe at external level $i$	chapter 29
${Fin}_{LE} (n)$	finite type of indices $k < n$ ; it has $n$ elements	chapter 29
${Lift}_{i} (A)$	explicit syntax raising a universe element one level	chapter 29
$El (a)$	type decoded from a Tarski code	chapter 75
$⌜ Π ⌝ (a, x . b)$	Tarski code for a dependent product	chapter 75
$e = e^{'}$	literal identity of raw syntax, before judgmental equality	chapter 75
$U_{1}, U_{0}$	large codes and small codes in the Hurkens interface	chapter 76
$Π_{1}, Π_{2}, Π_{0}, Π_{01}$	four product-code operations in that interface	chapter 76