On sets of terms with a given intersection type

Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Veneri [1981], we prove several facts about sets of terms having a given intersection type. One of our results is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair $(\Gamma,A)$ such that 1) $\Gamma \vdash M : A$ 2) $\Gamma \vdash N : A \Longrightarrow M =_{\beta\eta} N$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules. In the second part of the paper, we prove that the set of closed terms having a given intersection type is separable, and, if infinite, forms an adequate numeral system.