Семинар «Алгебра, геометрия и теория чисел»

Когда: суббота 21 марта, 17:00
Где: 322 АдмК

Гомотопическая теория типов как язык гомотопически когерентной математики (Аршак Айвазьян)

Интуиционистская теория типов (или теория типов Мартина-Лёфа, MLTT) — это альтернатива аксиоматической теории множеств. На первый взгляд для работающего математика разница между ними заключается лишь в косметической модификации нотации — более структуралистскими и индуктивными акцентами. Но внезапно эта модификация делает понятие равенства настолько более гибким, что оно может единообразно включать в себя как классическое равенство элементов множеств, так и изоморфизмы и эквивалентности. Это позволяет формально работать с бесконечно-категорными объектами так же, как и с классическими. Об этом стоит думать как о разовой «упаковке» мощного модельного инструментария внутри языка, вместо того чтобы постоянно заслонять идеи его техническими деталями.

В докладе я представлю современную экспозицию MLTT как языка локально декартово замкнутой категории с представимым естественным преобразованием предпучков. Я буду следовать главам 2 и 3 диссертации Даниэла Гратзера «Syntax and semantics of modal type theory». Затем будет введена аксиома унивалентности и мы обсудим особенности языка гомотопической теории типов, следуя HoTT Book.

Присоединяйтесь к ТГ группе семинара.

Адрес: МФТИ, Административный корпус, ауд. 322,
Первомайская ул. д.7, Долгопрудный.

#ВШМ_АГТЧ