En varias fuentes sobre la teoría de tipos intuicionista, el universo de tipos se toma como acumulado es decir $A:\mathcal U _i$ implica $A:\mathcal U_j$ siempre que $i\le j$ .
La pregunta es: ¿por qué tenemos que asumirlo? ¿Existe alguna dificultad inevitable si no lo utilizamos (así los elementos siempre tienen tipos únicos)? Y, ¿cuáles son las sutilezas implicadas en cada situación?
Gracias de antemano.
Se hace porque parece natural, y evita cierto tedio de tener que explicitar lift términos en un universo a un universo superior. Es esencialmente una restricción de subtipado, y en lugar de tener coerciones implícitas, se pueden tener coerciones explícitas, es decir, el lift s. Creo que una de las razones por las que Agda no lo hace tienen acumulatividad es que no interactúan bien con el polimorfismo del universo (o más bien sus interacciones no fueron bien entendidas), pero deberías comprobarlo. La subtipificación, en general, suele dar lugar a complejidades muy complicadas.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
