Хотбук 9.9

Ну для любой предкатегории C можно построить категорию C' вместе с функтором f : C -> C', который будет начальным таким функтором.

Я считаю, что категории всё-таки ближе к классическому понятию, по крайней мере, если рассматривать то, как они используются на практике. Дело в том, что у нас есть некоторая идея понятия категории, и мы пытаемся эту идею уложить в формальный фреймворк, и обычный фреймворк (ZFC) для этого не очень хорошо подходит, т.к. позволяет сформулировать только что-то похожее на предкатегории, но реально унивалентные категории гораздо ближе к этой идее. Не смотря на это, на практике всегда используется именно интуитивное понятие категории. Т.е. хоть формально у нас и предкатегории, но все притворяются, что у нас настоящии категории и заменяют изоморфизмы свободно на равенства.

Это можно сравнить с другим примером. Рассмотрим сетоиды. Мы бдуем говорить, что сетоид унивалентный, если эквивалентность на нем эквивалентна равенству. Легко видеть, что унивалентный сетоид — это то же самое, что множество. И наоборот, обычный сетоид можно определить через унивалентный (т.е. через множества). Сетоиды эквивалентны типу троек (X,C,f), где X — множество, C — унивалентный сетоид (т.е. тоже множество), а f : X -> C — сюръективная функция.

И еще один чуть менее вырожденый пример. Есть такое понятие как apartness relation, а еще есть tight apartness relation. Последнии будут выступать в роли унивалентной версии первых. Как обычно, tight apartness relation определяется через apartness relation, но можно сделать и наоборот. Тип множеств с apartness relation эквивалентен типу троек (X,C,f), где X — множество, C — множество с tight apartness relation, а f : X -> C — сюръективная функция.

Во всех этих примерах о множестве/типе X можно думать как о множестве, которое представляет элементы C. Например, C — это может быть множество термов с точностью до эквивалентности, а X — просто множество термов. Иногда ведь удобно работать именно с представлениями, а не с элементами C. Так же можно думать и о предкатегориях. Мы в конечном счете заинтересованы в подлежащей категории, но структура предкатегории — это доп. структура на ней, которая просто является некоторым представлением объектов, с которым может быть удобнее работать, например.

И еще один пример — это предпорядки и порядки, где порядки — это унивалентные предпорядки. Это частный случай примера предкатегорий/категорий, т.к. предпорядки — это в точности предкатегории, где все Hom-множества являются утверждениями, а порядки — это в точности категории с тем же свойством. Кстати, пример с сетоидами — это частный случай этого примера.

Еще предлагаю рассмотреть такой вопрос: когда моноид, рассматриваемый как предкатегория, является категорией? Ответ давать не буду, предлагаю подумать тем, кто не знает его.

Спасибо большое за весь этот рассказ

Всем здороу🍔). Я тип новичёк в этой вашей Теории категорий). Можете мне объяснить чё к чему по бырыку?)
Кароч, из определения википедии говориться, что один из трёх элементов монады это "функтор из категории K в себя". То есть монада содержит категорию как объект. Значит что монада - это категория категорий?

Многие построения основываются на наличии других постороений для их опредедения.
Можно считать, что категория - это параметр функтора, или элемент его структуры.

Однако в этом конкретном случае ответ - почти да. Есть категория, где (маленькие) категории выступают в качестве объектов, а функторы - в качестве морфизмов

https://ncatlab.org/nlab/show/Cat

Да, то есть эта категория К в монаде - есть малая категория?
И объектами категорий могут быть категории только если они маленькие? (на вскидку, ещё есть виды категорий?)

есть категория категорий побольше

https://ncatlab.org/nlab/show/CAT

Спасибо, буду перевиаривать и смареть линки!

по размеру я знаю только финитные, маленькие, локально маленькие и остальные

Понял, спасибо! Как раз что я и хотел услышать.
ну то есть в монаде используеться именно Cat (малая) категория?

Или не важно какая?

не важно

ПОНЯЛ СПС!

Cat как раз сама по себе не маленькая
Её объекты - маленькие