1 и 2 доклады мини-курса, продолжение следует.

За этим и другими курсам ассоциированными с Higher geometry можно следить (и, в частности, присоединяться к zoom-трансляциям) с соответствующего форума в телеграмме (можно попросить добавить вас любого участника, например, меня @arcsi)

— Симплициальные множества, нерв категории, сингулярное симплициальное множество, расслоения Кана, комплексы Кана, примеры

— Разница между теориями множеств и теориями типов

— Зависимые типы как расслоения Кана, зависимые термы как сечения (типы как комплексы Кана, термы как точки)
— Универсумы
— Семейства типов, зависимая сумма как тотальное пространство, зависимое произведение как пространство сечений
— Типа равенства как пространство путей, индукция по равенству, трансфер (как следствие индукции по равенству)
— Равенство и гомотопность функций, эквивалентность типов, аксиома унивалентности

— n-типы (-1 логика, 0 множества, 1 группоиды, ..), усечения

— Прекатегории, категории, примеры категорий

https://www.youtube.com/watch?v=1N-Fc1EQZAo
https://www.youtube.com/watch?v=6-GUJBvoQR4

Рассказ быстр и местами может быть неясен, если есть вопросы — пишите!