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

Когда: суббота 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 не будет опираться на аксиому выбора, в отличие от теоретико-множественного подхода.

Доклад будет наполнен несложными и красивыми доказательствами, позволяющими сделать этот язык поистине частью себя.