Лаборатория языковых инструментов

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

Докладчик: Валерий Исаев