Una visión general del Axioma de la Univalencia en la Teoría de Tipos Homotópica

Ponente(s): Marco Federico Larrea Schiavon

La Teoría de Tipos Homotópica (HoTT por sus siglas en inglés) es un lenguaje formal que consiste de objetos primitivos llamados tipos y de algunas reglas para manipularlos. Desde un punto de vista semántico, los tipos pueden ser considerados como espacios topológicos, desde una perspectiva homotópica. Esto significa que en el lenguaje de HoTT solo podremos hablar sobre propiedades homotópicas de espacios como, por ejemplo, trayectorias y homotopías. El Axioma de la Univalencia es un fortalecimiento adicional de HoTT propuesto por Vladimir Voevodsky. En pocas palabras, nos permite caracterizar el tipo de trayectorias entre dos tipos como el tipo de equivalencias entre ellos. Esto resulta ser una adición muy poderosa y útil a HoTT. En esta ponencia, daré una breve introducción a HoTT sin profundizar en los detalles sintácticos. Después de esto, daré una declaración formal del Axioma de la Univalencia y discutiremos algunas de sus implicaciones. No se requieren conocimientos previos de lógica ni de Teoría de Tipos. Sin embargo, me basaré en algunas nociones básicas de los espacios topológicos y de Teoría de Homotopía para guiar la intuición.