Teoría Homotópica de Tipos
Parte IV
Notas del curso de Interactive Theorem Provers, dictado por Paige North en la Escuela de Ciencias Informáticas (ECI) 2025, Buenos Aires. El enfoque práctico del curso utilizó el asistente de pruebas Rocq; el enfoque teórico siguió el desarrollo de la teoría homotópica de tipos (HoTT). Las notas aquí presentadas siguen el desarrollo lógico-teórico: desde la deducción natural y el lambda cálculo tipado, pasando por los tipos inductivos y el tipo identidad, hasta los niveles de homotopía y los tipos inductivos superiores. Los ejercicios prácticos del curso están disponibles en GitHub.
- 1. Introducción y Notación
- 2. Deducción Natural y Lambda Cálculo
- 3. Tipos Inductivos
- 4. Lógica de Primer Orden en Teoría de Tipos
- 5. Aritmética en Teoría de Tipos
- 6. Propiedades del Tipo Identidad
- 7. Niveles de Homotopía y Equivalencias
- 8. Tipos Inductivos Superiores
- 9. Introduccion a Rocq
- 10. Expresividad: Matemáticas en UniMath
- 11. Bibliografía