Homotopie-Typentheorie (HoTT)

Ein fundamentales Rahmenwerk, das die Typentheorie homotopisch interpretiert: Typen gelten als Räume (oder ∞-Gruppoide), Terme als Punkte und Gleichheiten als Pfade, wodurch logische Typenkonstruktoren mit homotopietheoretischer Semantik verschmelzen.