Libros introductorios como preparación para leer el libro de teoría de la homotopía de Voevodsky (HoTT)

Question

Me gustaría leer Libro Voevodsky HoTT .

Sin embargo, me faltan muchas cosas básicas. Necesitaría primero algunos libros introductorios que cubran temas como los groupoides, las fibraciones, los tipos W y la teoría de la homotopía.

¿Alguna sugerencia de referencias? (Estoy buscando principalmente libros)

Por favor, no se trata de un libro escrito por muchos autores de igual importancia. Así que más específico: "El libro HoTT escrito por los participantes del Año Especial sobre Fundamentos Univalentes en el Instituto de Estudios Avanzados".

Answer 1

Puedes echar un vistazo a las conferencias de Robert Harper: http://www.cs.cmu.edu/~rwh/cursos/hott/ (Hay apuntes de clase y grabaciones de vídeo) Requieren mucho menos de lo que has descrito para entender y encubrir el HoTT.

Answer 2

Otra forma de ver esas nociones de groupoides y fibraciones es que la teoría de tipos te dice lo que son . Lo hace diciéndole lo que puedes hacer con ellos .

Por ejemplo, con las fibraciones, se pueden transportar puntos en las fibras a lo largo de caminos -- esto es exactamente la intención de la noción clásica de fibraciones. Esto es aún más cierto en el caso de las $\infty$ -groupoides.

Así, en lugar de leer un montón de material "de fondo" que te explique las versiones clásicas de los términos que se utilizan en el libro de HoTT, puede que te resulte más fácil y rápido aprender lo que son a través de las explicaciones que ofrece el libro.

Si no te sientes cómodo con la idea de aprender lo que son las cosas aprendiendo lo que puedes hacer con ellas, te sugeriría que empezaras a leer sobre la propia teoría de la homotopía. La topología algebraica de Hatcher es probablemente un punto de partida razonable (que está disponible gratuitamente en línea).

Answer 3

Realmente recomiendo Awodey's Teoría de la categoría ya que su tratamiento es especialmente adecuado para entender la conexión entre la teoría de tipos de Martin-Lof y las categorías cerradas localmente cartesianas. Personalmente, estaría perdido tratando de entender el libro de HoTT (por el que no se le puede dar a Voevodsky ni mucho menos el único crédito) sin la cobertura de Awodey del cálculo lambda tipado.

En cuanto a la cuestión de la estructura de los grupos, se puede navegar un poco por nLab para hacerse una idea (concretamente los autores parecen interpretar los tipos HoTT como complejos Kan/ $\infty$ -groupoides), o podrías leer el primer par de capítulos de "Higher Topos Theory" de Jacob Lurie, que puedes encontrar en su página web. No es necesario saber muchas cosas profundas sobre homotopía o complejos de Kan para leer el libro de HoTT, pero entender la idea de un complejo de Kan hace que la idea detrás de los tipos de identidad sea mucho más transparente.