Teoría Homotópica de Tipos - Fernando Chu (Tesis de Maestría)

En estas páginas pueden encontrar la formalización en Agda del contenido de mi tesis de maestría. El pdf lo pueden encontrar en el siguiente link.

Capítulos

• Capítulo 1 - Preliminares categóricos
• Capítulo 2 - Teoría de Tipos Dependientes
• Capítulo 3 - La Interpretación Homotópica
• Capítulo 4 - Teoría Homotópica de Tipos
• Capítulo 5 - Conclusiones

El código de todo el material para la creación de la página web y del pdf se encuentra libremente en un repositorio abierto.

Agradecimientos

Agradezco a la nuevamente a la comunidad HoTT por su voluntad de compartir su conocimiento. Para el desarrollo de agda, tomé como referencia múltiples fuentes, incluyendo las notas del Profesor Escardo, la formalización del Profesor Rijke de su libro, la librería agda-unimath, la librería HoTT-Agda, y la librería estándar de Agda.