Creo que no hay ninguna regla de formación para el tipo de cociente. ¿Cómo se construye un conjunto cociente en la teoría de tipos de Martin-Löf?
Respuesta
¿Demasiados anuncios?
El enfoque tradicional de los cocientes en la teoría de tipos es evitarlos por completo utilizando en su lugar setoides. En este enfoque equipamos un tipo $X$ con una relación de equivalencia $E$ para conseguir un setoid , que es sólo el par $(X, E)$ . Si $(X, E)$ y $(X', E')$ son setoides, decimos que un operación es un mapa $X \to Y$ y un función es una operación que también preserva las relaciones de equivalencia. Si queremos hacer el cociente de un setoide $(X, E)$ por una relación de equivalencia $F$ No tocamos $X$ en absoluto, sino que sustituimos $E$ con la nueva relación de equivalencia (típicamente mayor) $F$ .
Un enfoque más moderno es extender la teoría de tipos pero añadiendo tipos cotizados. Esto se hizo para la teoría de tipos extensional en, por ejemplo, Maietti, Correspondencia modular entre teorías de tipo teorías de tipos y categorías dependientes, incluyendo pretopoi y topoi . Los tipos cocientes también se incluyen en la teoría de tipos de homotopía, como una especie de tipo inductivo superior.
