Estoy leyendo sobre la teoría de los tipos dependientes en el libro en línea de la teoría de tipos de homotopía .
En la sección 1.3 del capítulo de Teoría de tipos , introduce la noción de jerarquía de universos : , donde
cada universo es un elemento del próximo universo . Además, suponemos que nuestros universos son acumulativos, es decir, que todos los elementos del universo también son elementos del universo .U i + 1 i t h (i+1 ) t h
Sin embargo, cuando miro las reglas de formación para los diversos tipos en el apéndice A, a primera vista, si un universo aparece sobre la barra como premisa, el mismo universo aparece debajo. Por ejemplo, para la regla de formación de tipos de coproductos:
Entonces mi pregunta es ¿por qué es necesaria una jerarquía? ¿En qué circunstancias necesitas saltar de un universo a uno más alto en la jerarquía? Realmente no es obvio para mí cómo dada cualquier combinación de , puede terminar con un tipo que no está en . En más detalles: las reglas de formación en las secciones del apéndice A.2.4, A.2.5, A.2.6, A.2.7, A.2.8, A.2.9, A.2.10, A.3.2, ya sea mencionar en la premisa y el juicio, o simplemente en el juicio. BU i
El libro también sugiere que hay una forma formal de asignar universos:
Si hay alguna duda sobre si un argumento es correcto, la forma de verificarlo es intentar asignar niveles consistentemente a todos los universos que aparecen en él.
¿Cuál es el proceso para asignar niveles consistentemente?
llevaría a la paradoja de RussellU j U i j>i . Evitar la paradoja de Russell se menciona explícitamente en el libro (página 24). También entra en más detalles en la página 54, 55, que utiliza "universos de estilo Russell" en lugar de "universos de estilo Tarski". Entonces, a un nivel muy alto, doy por sentado que la teoría quiere evitar la paradoja. Desafortunadamente no tengo los antecedentes para entenderlo directamente. Lo que busco en esta pregunta, en realidad, es solo arañar la superficie al obtener algunos ejemplos de cosas en y no en para y puede ser cualquier otra cosa que me dé una idea sobre cómo funcionan las jerarquías.
Respuestas:
La pregunta bajo qué circunstancias necesitamos saltar de un universo a uno más alto en la jerarquía es buena. Tener la jerarquía y la capacidad de escalarlo es importante. Necesitas saltar niveles cuando quieras tratar un universo como un tipo o como parte de un tipo. Por ejemplo, para definir funciones de tipo (no dependiente) , debe mostrar que A → U i está en un universo. Pero eso no puede ser U i o algún universo más pequeño. ¿Asi que que hacemos? Para lidiar con el problema (sin usar el U i : U i ), necesitamos saltar un universo. La regla que nos permite hacer este salto es U
fuente
fuente