集合体

在数学中，集合体（X，~）是一个配备有等价关系~的集合（或类型）X。拟集也可称为E集、主教集或扩展集。集合体尤其在证明理论和数学的类型理论基础中被研究。在数学中，当人们在一个集合上定义一个等价关系时，通常会立即形成商集（将等价变成平等）。相反，当必须保持同一性和等价性之间的差异时，可以使用集合体，通常是用扩展的平等（原始集合上的平等）和扩展的平等（等价关系，或商集合上的平等）来解释。

在证明理论中，特别是基于库里-霍华德对应关系的构造数学的证明理论中，人们常常将一个数学命题与它的证明集（如果有的话）联系起来。当然，一个给定的命题可能有许多证明；根据证明无关性原则，通常只有命题的真实性才是重要的，而不是哪一个证明被使用。然而，库里-霍华德对应关系可以把证明变成算法，而算法之间的差异往往是重要的。因此，证明理论家可能更倾向于将一个命题与一个证明的集合体相识别，如果证明可以通过β转换或类似的方式相互转换，则认为它们是等价的。

在数学的类型理论基础中，setoids可能被用于缺乏商数类型的类型理论中，以模拟一般的数学集合。例如，在佩尔-马丁-勒夫的直觉类型理论中，没有实数的类型，只有有理数的规则考奇序列的类型。因此，要在马丁-洛夫的框架内进行实数分析，就必须使用一个实数集合体，即具有通常的等价概念的有规律的考奇序列类型。实数的谓词和函数需要为正则Cauchy序列定义，并证明其与等价关系兼容。通常（尽管这取决于所使用的类型理论），选择公理对于类型之间的函数（扩展函数）是成立的，但对于集合体之间的函数（扩展函数）则不成立。集合一词被不同程度地用作类型的同义词或setoid的同义词。

在构造数学中，人们常常把一个具有不等价关系而不是等价关系的集合体称为构造集合体。有时人们也考虑使用部分等价关系或部分不等价关系的部分集合体。(例如，见Barthe等人，第1节)