Введение
Математическая конструкция множества с отношением эквивалентности
В математике сетоид (X, ~) — это множество (или тип) X, снабжённое отношением эквивалентности ~. Сетоид также может называться E-множеством, множеством Бишопа или расширенным множеством. Сетоиды особенно изучаются в теории доказательств и в теоретико-типовых основаниях математики. Часто в математике, когда на множестве определяется отношение эквивалентности, сразу же формируется фактормножество (преобразуя эквивалентность в равенство). В отличие от этого, сетоиды могут использоваться, когда необходимо сохранять различие между тождеством и эквивалентностью, часто с интерпретацией интентционального равенства (равенство в исходном множестве) и экстенсионального равенства (отношение эквивалентности или равенство в фактормножестве).
Теория доказательства
В теории доказательств, особенно в теории доказательств конструктивной математики, основанной на соответствии Карри — Ховарда, математическое утверждение часто отождествляется с множеством его доказательств (если они существуют). Очевидно, что данное утверждение может иметь множество доказательств; согласно принципу нерелевантности доказательств, обычно важна лишь истинность утверждения, а не конкретное использованное доказательство. Однако соответствие Карри — Ховарда может превращать доказательства в алгоритмы, а различия между алгоритмами часто имеют значение. Поэтому теоретики доказательств могут предпочитать отождествлять утверждение с сетоидом доказательств, рассматривая доказательства как эквивалентные, если их можно преобразовать друг в друга посредством бета-редукции или аналогичных операций.
Теория типов
В теоретических основаниях математики сетоиды могут использоваться в теории типов, не имеющей типов частных, для моделирования общих математических множеств. Например, в интуиционистской теории типов Пер Мартина Лёфа отсутствует тип действительных чисел, есть только тип регулярных последовательностей Коши рациональных чисел. Следовательно, для проведения вещественного анализа в рамках Лёфа необходимо работать с сетоидом действительных чисел – типом регулярных последовательностей Коши, снабженным обычным понятием эквивалентности. Предикаты и функции над действительными числами должны быть определены для регулярных последовательностей Коши и доказано, что они согласованы с отношением эквивалентности. Как правило (хотя это зависит от используемой теории типов), аксиома выбора выполняется для функций между типами (интенсиональные функции), но не для функций между сетоидами (экстенсиональные функции). Термин "множество" используется по-разному, как синоним "тип" или как синоним "сетоид".
Конструктивная математика
В конструктивной математике часто рассматривают сетоид с отношением отчуждения вместо отношения эквивалентности, называемый конструктивным сетоидом. Иногда также рассматривают частичный сетоид, использующий частичное отношение эквивалентности или частичное отчуждение (см., например, Barthe et al., раздел 1).