appendix sectionnotation

Judgments and contexts

symbol	meaning	first
symbol	meaning	first
$Γ ctx$	$Γ$ is a well-formed context	chapter 2
$Γ ⊢ A type$	$A$ is a type in context $Γ$	chapter 26
$Γ ⊢ a : A$	$a$ has type $A$ under declarations $Γ$	chapter 2
$Γ ⊢ A \equiv B type$	judgmental equality of types	chapter 26
$Γ ⊢ a \equiv b : A$	judgmental equality of terms	chapter 26
$f : Θ \Rightarrow_{Γ} Δ$	relative telescope map over $Γ$	chapter 26
$Γ ⊢ γ : Δ$	substitution from $Γ$ to $Δ$	chapter 54
$Γ ⊢ γ \equiv δ : Δ$	equality of substitutions	chapter 54
${TyEq}_{i} (A, B)$	Nuprl-style semantic equality of closed types at stratum $i$	chapter 36
${MemEq}_{i} (a, b; A)$	Nuprl-style PER equality of closed members of $A$	chapter 36
${Mem}_{i} (a; A)$	Nuprl-style closed membership	chapter 36
$\cdot$	empty context	chapter 2