Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result 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. Moreover, we show that the set of closed terms with a given type is uniformly separable, and, if infinite, forms an adequate numeral system. The proof of this fact uses an internal version of the B\"ohm-out technique, adapted to terms of a given intersection type.

翻译：在Coppo、Dezani-Ciancaglini和Venneri[1981年]的交叉类型分配系统中,我们用一个变式来工作,我们证明关于具有特定交叉类型的各种术语的几种事实。我们的主要结果是,每个强烈正常化的 M 术语都接受一个uniquenity type *,这是一对美元(Gamma,A),因此1,$\Gamma\vdash M:A$2,$Gamma\vdash N:A\Longrightrightrow M ⁇ beta\eta}N$1,我们还讨论多个交叉类型代数的演示,以及相应的类型分配规则选择。此外,我们表明,与特定类型封闭的术语是统一的,如果是无限的,则形成一个适当的数字系统。这个事实的证据使用了一个内部版本的B\'ohm-out技术,适应了特定交叉类型的条款。