appendix sectionnotation

Homotopy type theory

symbol	meaning	first
symbol	meaning	first
$p \cdot q$	path concatenation	chapter 30
$p^{- 1}$	inverse path	chapter 30
$ap, apd$	action on paths, dependent action	chapter 30
$tr$	transport	chapter 30
$f \sim g$	homotopy of functions	chapter 62
$A ≃ B$	equivalence of types	chapter 62
$isEquiv (f)$	$f$ is an equivalence	chapter 62
$isContr (A)$	$A$ is contractible	chapter 62
$isProp (A), isSet (A)$	$A$ is a proposition or a set	chapter 66
$is - n - type (A)$	$A$ is an $n$ -type	chapter 66
$fib (f, b)$	fiber of $f$ over $b$	chapter 62
$idtoeqv, ua$	identity-to-equivalence and its univalent inverse	chapter 65
$happly$	apply a function equality pointwise	chapter 30
$‖ A ‖_{n}$	$n$ -truncation	chapter 66
$‖ A ‖$	propositional truncation	chapter 66
$\| a \|$	point constructor of a truncation	chapter 66
$Ω, S^{n}$	loop space and $n$ -sphere	chapter 68, chapter 69
$loop$	loop path at a chosen basepoint	chapter 79
$base$	base-point constructor of the circle	chapter 68
$Susp, N, S, merid$	suspension and its constructors	chapter 68
$Z$	metatheoretic integers used in an external model	chapter 54
$Z$	integers	chapter 69
$\| A \|$	cardinal-equivalence class of a set $A$	chapter 76
$Set$	internal type of small sets	chapter 74
${Set}_{U}$	internal category of small sets	chapter 74