Type formers and terms

In the Timpl entries below, (e) and (r) range over explicitness and relevance.

symbol	meaning	first
symbol	meaning	first
$\prod _{x:A}B$	dependent product	chapter 22
$\prod _{x:A}^{e,r}B$	product with explicitness and relevance	chapter 48
$\mathrm{\Gamma }⊢A\dot{\in }{\mathcal{U}}_{\ell }$	suspended universe-formation guard	chapter 50
$\sum _{x:A}B$	dependent sum	chapter 27
${\mathsf{W}}_{x:A}B$	well-founded tree type	chapter 28
${\mathsf{Eq}}_A(a,b)$	extensional equality type	chapter 35
${\mathsf{Id}}_A(a,b)$	identity type; extensional only in a declared source calculus	chapter 28
$a{=}_{A}b$	path-language form of identity	chapter 62
$\mathbf{1},\mathbf{0},\mathbf{2},\mathbb{N}$	unit, empty, Boolean, and natural-number types	chapter 27–chapter 28
$\lambda (x:A).b$	kernel abstraction with domain annotation	chapter 22
${\lambda }^{e,r}x.b$	surface abstraction with binder metadata	chapter 48
${\lambda }^{e,r}(x:A).b$	annotated abstraction with binder metadata	chapter 48
$f{}^{e,r}a$	application with copied binder metadata	chapter 48
$\lambda x.b$	ordinary unannotated abstraction where the fixed syntax permits it	chapter 2
$\mathrm{\Lambda }X.b$	PTS spelling of explicit type abstraction	chapter 22
$\lambda u::\kappa .A$	PTS spelling of constructor abstraction	chapter 22
$(a,b)$	dependent pair	chapter 27
${\mathsf{pr}}_1,{\mathsf{pr}}_2$	first and second projection	chapter 27
$\star$	the element of $\mathbf{1}$	chapter 27
$\mathsf{tt},\mathsf{ff}$	Boolean constructors	chapter 28
$\mathsf{0},\mathsf{suc}$	natural-number constructors	chapter 28
$\mathsf{inl},\mathsf{inr}$	coproduct constructors	chapter 28
$\mathsf{sup}$	W-type constructor	chapter 28
${\mathsf{ind}}_A$	dependent eliminator for $A$	chapter 28
${\mathsf{rec}}_A$	nondependent recursor for $A$	chapter 28
${\mathsf{rec}}_{\mathbf{0}}$	schematic recursor from $\mathbf{0}$; expected type fixes its target	chapter 28
${\mathcal{T}}_{\mathrm{D}}$	extensional source calculus for Dybjer’s theorem	chapter 28
$\mathsf{funext}$	function extensionality map in ${\mathcal{T}}_{\mathrm{D}}$	chapter 28
${\nu }_X$	natural container-normal-form isomorphism for $\mathrm{\Phi }(X)$	chapter 28
${\iota }_{\mathrm{\Phi }}$	initial algebra structure transported to a W-type	chapter 28
$\mathsf{refl}$	reflexivity constructor	chapter 30
$\mathsf{J}$	identity eliminator	chapter 30
$\mathsf{K}$	uniqueness-of-identity eliminator	chapter 30