Урок Второй. Построение категорий от Set до Инфинити!
После первой 2-часовой лекции по MLTT, где детально разбираются Пи, Сигма, Путь и все их компоненты Formation/Inro/Elim/Rec/Case/Induction/Eta/Beta (а у Пути еще дополнительных куча subst, trans, все конечно через J выражаются, но через J реально никто не пишет, поэтому надо учить сразу культурке). У Пи типа есть еще funExt аксиома без которой не доказывается, что тип морфизмов является множеством, поэтому конструктивное построение инфинити категорий было невозможно до agda --cubical. Если морфизмы образуют не множество, а групоид, то это уже будет другая категория и так дальше до инфинити групоида. Кроме этого категории еще вкладываются друг в друга, например 0-категория — это множества или сетоид, где отношение Hom A B — это отношение эквивалентности на множествах, 1-категория, это категория где объекты — это 0-категории, множества или топологические пространства, а морфизмы — это отображения, в 2-категориях объекты — это 1-категории или просто категории, 1-морфизмы — это функторы, а 2-морфизмы — это естественные преобразования. На втором уроке можно уже строить категорию Множеств. Ну а категорию функторов можно давать уже после полного введения в теорию категори с лимитами. И уже только после теорката и категории функторов можно прееходить к семантике зависимой теории, категории контекстов, где морфизмы — это подстановки и категориям с семействами. Только сейчас решил написать это.
