Исследовательская группа
Лаборатория языковых инструментов
Базовые концепции гомотопической теории типов
September 23
В данном докладе мы обсудим отличия
гомотопической и обычной теорий типов. Мы рассмотрим несколько
конструкций, которые определяются в HoTT (такие как пропозициональное
обрезание, фактор-типы и аксиома унивалентности), и примеры их
использования. В частности, мы рассмотрим пример сортировки списков
тотально упорядоченных элементов, который показывает необходимость
определения дизъюнкции через джойны.
Докладчик: Валерий Исаев