Семинар «Алгебра, геометрия и теория чисел» Когда: суббота 28 марта, 17:00 Где: 322 АдмК Гомотопическая теория типов как язык гомотопически когерентной математики (Аршак Айвазьян) В первой части мы определили интенсиональную теорию типов с базовыми связками (Prod, Sigma), терминальным типом (1), индуктивными типами (N, coprod, 0, =) и кумулятивной иерархией универсумов (U_n), а также обсудили семантику большинства из них. Во второй части мы перейдем непосредственно к гомотопической теории типов и обсудим такие темы, как: 1) гомотопическая эквивалентность типов и аксиома унивалентности; 2) иерархия n-типов: contractible = (-2)-type < propositional = (-1)-type < set = 0-type < 1-type < 2-type < ... и рефлекторы на них, заданные как высшие индуктивные типы (HITs), которые семантически соответствуют этажам башни Постникова; 3) ортогональная система факторизации n-связных и n-усеченных стрелок, обобщающая факторизацию на сюръекции и вложения при n = -1; 4) последовательность Пуппе и длинная точная последовательность расслоения; 5) единство понятий равенства, изоморфизма и эквивалентности 1-категорий, вплоть до так называемой основной теоремы теории категорий, чье доказательство в HoTT не будет опираться на аксиому выбора, в отличие от теоретико-множественного подхода. Доклад будет наполнен несложными и красивыми доказательствами, позволяющими сделать этот язык поистине частью себя.