Teoría Homotópica de Tipos: ¿Fundamento de las matemáticas?

La teoría homotópica de tipos (HoTT) es un sistema formal que ha ganado notoriedad por su propuesta como un nuevo fundamento de las matemáticas. Sin embargo, el uso de conceptos avanzados de topología y teoría de homotopía como conceptos básicos dificulta su adopción. En este artículo introduzco al lector a esta discusión, haciendo primero un repaso formal e histórico de HoTT, su teoría de tipos y sus nociones topológicas. Finalmente, discuto las dos propuestas más relevantes en la literatura como justificación informal e intuitiva de HoTT, junto a las críticas y problemas que deben enfrentar ambas propuestas para lograr su objetivo.