En la teoría de tipos , una especie de fundamento de las matemáticas, un tipo de cociente es un tipo de datos algebraicos que representa un tipo cuya relación de igualdad ha sido redefinida por una relación de equivalencia dada, de modo que los elementos del tipo se dividen en un conjunto de clases de equivalencia cuyo La cardinalidad es menor o igual que la del tipo base. Así como los tipos de producto y los tipos de suma son análogos al producto cartesiano y la suma disjunta de estructuras algebraicas abstractas, los tipos de cociente reflejan el concepto de cocientes de teoría de conjuntos, conjuntos cuyos elementos están divididos de forma sobreyectiva en clases de equivalencia por una relación de equivalencia dada en el conjunto. Las estructuras algebraicas cuyo conjunto subyacente es un cociente también se denominan cocientes. Ejemplos de tales estructuras de cocientes incluyen conjuntos de cocientes , grupos , anillos , categorías y, en topología, espacios de cocientes .
En las teorías de tipos que carecen de tipos de cociente, a menudo se utilizan setoides (conjuntos equipados explícitamente con una relación de equivalencia).