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. 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.

翻译：在Coppo、Dezani-Ciancaglini和Veneri[1981年]的交叉类型分配系统中,我们用多种不同的办法,证明关于具有特定交叉类型的各种术语的多个事实。我们的主要结果是,每个严格正常化的术语$M$都接受“独一”打字*,这是一对$(Gamma,A),因此1美元=Gamma\vdash M:A$2,$Gamma\vdash N:A\Longrightright M ⁇ beta\eta}N$。我们还讨论了若干交叉型代数的表述,以及相应的类型分配规则的选择。