Гомотопічна теорія типів

Гомотопічна теорія типів — спеціальна синтетична конструктивна версія теорії гомотопій, що дозволяє безпосередньо оперувати багатовимірними рівностями у вигляді кубів.