Loading article…
数学において、セットイド( X , ~) は、同値関係~を備えた集合(または型) Xである。セットイドは、 E-セット、ビショップセット、または拡張セットとも呼ばれる。[ 1 ]
セットイドは、特に証明論や数学の型理論的 基礎において研究されています。数学では、集合上で同値関係を定義すると、すぐに商集合が形成されます（同値関係が等式に変換されます）。これに対し、セットイドは、同一性と同値性の違いを維持する必要がある場合に使用され、多くの場合、内包的等式（元の集合上の等式）と外延的等式（同値関係、または商集合上の等式）の解釈が用いられます。
証明論、特にカリー・ハワード対応に基づく構成的数学の証明論では、数学的命題をその証明の集合（存在する場合）と同一視することがよくある。もちろん、与えられた命題には多くの証明が存在する可能性がある。証明無関係の原理によれば、通常、どの証明が用いられたかではなく、命題の真偽のみが重要となる。しかし、カリー・ハワード対応は証明をアルゴリズムに変換することができ、アルゴリズム間の違いはしばしば重要となる。そのため、証明論者は、ベータ変換などによって相互に変換できる証明を同等とみなし、命題を証明の集合と同一視することを好む場合がある。
数学の型理論的基礎において、セトイドは、商型を持たない型理論において、一般的な数学的集合をモデル化するために用いられることがある。例えば、ペル・マルティン＝レーフの直観主義型理論では、実数の型はなく、有理数の正則コーシー列の型のみが存在する。したがって、マルティン＝レーフの枠組みで実解析を行うには、実数のセトイド、すなわち通常の同値概念を備えた正則コーシー列の型を扱う必要がある。実数の述語と関数は、正則コーシー列に対して定義され、同値関係と両立することが証明されなければならない。通常（ただし、使用する型理論にもよる）、選択公理は型間の関数（内包関数）には成り立つが、セトイド間の関数（外延関数）には成り立たない。「集合」という用語は、「型」の同義語として、あるいは「セトイド」の同義語として様々に用いられる。[ 2 ]
構成的数学では、同値関係の代わりに分離関係を持つ集合体（構成的集合体と呼ばれる）を用いることが多い。部分同値関係や部分分離関係を用いた部分集合体を考える場合もある（例えば、Barthe et al.、第1節を参照）。