Teoría de Tipos Homotópicos (HoTT)

Un marco fundacional que interpreta la teoría de tipos de forma homotópica: los tipos se tratan como espacios (o ∞-grupoides), los términos como puntos y las igualdades como caminos, combinando constructores lógicos de tipos con semántica homotópica.