En matemáticas , un setoide ( X , ~) es un conjunto (o tipo ) X dotado de una relación de equivalencia ~. Un setoide también puede denominarse E-conjunto , conjunto de Bishop o conjunto extensional . [1]
Los setoides se estudian especialmente en la teoría de la demostración y en los fundamentos de la teoría de tipos de las matemáticas . A menudo, en matemáticas, cuando se define una relación de equivalencia en un conjunto, se forma inmediatamente el conjunto cociente (convirtiendo la equivalencia en igualdad ). Por el contrario, los setoides pueden usarse cuando debe mantenerse una diferencia entre identidad y equivalencia, a menudo con una interpretación de la igualdad intensional (la igualdad en el conjunto original) y la igualdad extensional (la relación de equivalencia o la igualdad en el conjunto cociente).
En la teoría de la prueba, particularmente la teoría de la prueba de las matemáticas constructivas basada en la correspondencia Curry-Howard , a menudo se identifica una proposición matemática con su conjunto de pruebas (si las hay). Una proposición dada puede tener muchas pruebas, por supuesto; de acuerdo con el principio de irrelevancia de la prueba, normalmente solo importa la verdad de la proposición, no qué prueba se utilizó. Sin embargo, la correspondencia Curry-Howard puede convertir las pruebas en algoritmos , y las diferencias entre algoritmos suelen ser importantes. Por lo tanto, los teóricos de la prueba pueden preferir identificar una proposición con un conjunto de pruebas, considerando que las pruebas son equivalentes si se pueden convertir entre sí mediante la conversión beta o similar.
En los fundamentos teóricos de tipos de las matemáticas, los setoides pueden usarse en una teoría de tipos que carece de tipos cocientes para modelar conjuntos matemáticos generales. Por ejemplo, en la teoría de tipos intuicionista de Per Martin-Löf , no hay ningún tipo de números reales , solo un tipo de secuencias regulares de Cauchy de números racionales . Por lo tanto, para hacer un análisis real en el marco de Martin-Löf, uno debe trabajar con un setoide de números reales, el tipo de secuencias regulares de Cauchy equipadas con la noción habitual de equivalencia. Los predicados y funciones de números reales deben definirse para secuencias regulares de Cauchy y demostrarse que son compatibles con la relación de equivalencia. Típicamente (aunque depende de la teoría de tipos utilizada), el axioma de elección se cumplirá para funciones entre tipos (funciones intensionales), pero no para funciones entre setoides (funciones extensionales). [ aclaración necesaria ] El término "conjunto" se usa de diversas formas, ya sea como sinónimo de "tipo" o como sinónimo de "setoide". [2]
En matemáticas constructivas , a menudo se toma un setoide con una relación de separación en lugar de una relación de equivalencia, lo que se denomina setoide constructivo . A veces también se considera un setoide parcial utilizando una relación de equivalencia parcial o separación parcial (véase, por ejemplo, Barthe et al. , sección 1).