appendix sectionnotation

Relational parametricity

symbol	meaning	first
symbol	meaning	first
$Tm (A)$	beta-classes of closed terms of type $A$	chapter 6
$R : A \leftrightarrow B$	relation between closed typed beta-classes	chapter 6
$R \Rightarrow S$	arrow lifting of two relations	chapter 6
$ϱ : ϱ_{0} \leftrightarrow ϱ_{1} over Δ$	relational type environment with two endpoints	chapter 6
$[[A {]]}_{ϱ}$	relational interpretation of a type	chapter 6
${Eq}_{A}, Gr (k)$	beta identity and graph relations	chapter 6
$γ_{0} [[Γ {]]}_{ϱ} γ_{1}$	related closing term substitutions	chapter 6