Семинар «Алгебра, геометрия и теория чисел» Когда: суббота 21 марта, 17:00 Где: 322 АдмК Гомотопическая теория типов как язык гомотопически когерентной математики (Аршак Айвазьян) Интуиционистская теория типов (или теория типов Мартина-Лёфа, MLTT) — это альтернатива аксиоматической теории множеств. На первый взгляд для работающего математика разница между ними заключается лишь в косметической модификации нотации — более структуралистскими и индуктивными акцентами. Но внезапно эта модификация делает понятие равенства настолько более гибким, что оно может единообразно включать в себя как классическое равенство элементов множеств, так и изоморфизмы и эквивалентности. Это позволяет формально работать с бесконечно-категорными объектами так же, как и с классическими. Об этом стоит думать как о разовой «упаковке» мощного модельного инструментария внутри языка, вместо того чтобы постоянно заслонять идеи его техническими деталями. В докладе я представлю современную экспозицию MLTT как языка локально декартово замкнутой категории с представимым естественным преобразованием предпучков. Я буду следовать главам 2 и 3 диссертации Даниэла Гратзера «Syntax and semantics of modal type theory». Затем будет введена аксиома унивалентности и мы обсудим особенности языка гомотопической теории типов, следуя HoTT Book. Присоединяйтесь к ТГ группе семинара. Адрес: МФТИ, Административный корпус, ауд. 322, Первомайская ул. д.7, Долгопрудный. #ВШМ_АГТЧ