Не секрет, что формализация математики, логики, языков программирования, а также верификация программ с использованием теории типов наталкивается на сложности работы с иерархией равенств в теории типов. Научный фольклор не случайно пестрит упоминаниями «геенны сетоидной». При этом, чем больше термов вычислительно равны, т.е. неразличимы в используемой формальной системе, тем проще с ней работать на практике — как в смысле сокращения ручного труда, так и увеличения производительности проверки типов, например, при использовании рефлексивных доказательств. В особенности это справедливо для термов, интерпретируемых как доказательства неразличимости высказываний. Однако, безыскусное внедрение неразличимости доказательств в теорию типов приводит либо к потере разрешимости проверки типов, либо к потере совместимости с другими расширениями базовой теории, такими как Унивалентность.
Первая часть доклада подготовит почву для освещения основной темы: в частности будет рассмотрена структура вселенных в системе интерактивных доказательств Coq. Во второй части пойдет речь об относительно недавно добавленной экспериментальной вселенной строгих высказываний SProp с неразличимыми по определению доказательствами. При этом сохраняются перечисленные выше желательные свойства и показывается неадекватность известного подхода одиночной элиминации во вселенной Prop для настоящей проблемы. Также будет показана связь SProp с другими вселенными на простых примерах.