Не секрет, что формализация математики, логики, языков программирования, а также верификация программ с использованием теории типов наталкивается на сложности работы с иерархией равенств в теории типов. Научный фольклор не случайно пестрит упоминаниями "геенны сетоидной". При этом, чем больше термов вычислительно равны, т.е. неразличимы в используемой формальной системе, тем проще с ней работать на практике -- как в смысле сокращения ручного труда, так и увеличения производительности проверки типов, например, при использовании рефлексивных доказательств. В особенности это справедливо для термов, интерпретируемых как доказательства неразличимости высказываний. Однако, безыскусное внедрение неразличимости доказательств в теорию типов приводит либо к потере разрешимости проверки типов, либо к потере совместимости с другими расширениями базовой теории, такими как унивалентность.

Первая часть доклада подготовит почву для освещения основной темы: в частности будет рассмотрена структура вселенных в системе интерактивных…

https://www.youtube.com/watch?v=90RajY2nrgk :)