Título: Teoría Homotópica de Tipos en Agda

Directora: Dra. Gabriela Steren

Jurados: Dra. Cecilia Manzino, Dr. Miguel Pagano, Dr. Álvaro Tasistro

Resumen:

El objetivo de esta tesis es desarrollar una implementación computacional de diversos conceptos presentes en la teoría homotópica de tipos, incluyendo un estudio de distintas nociones de finitud en la lógica intuicionista, e implementar demostraciones constructivas de sus propiedades. Se propone formalizar los resultados en el asistente de demostración Agda, eligiendo como formalismo en particular el sistema conocido como Homotopy type theory (HoTT).