есть задачник по сабжу?

Ну моё утверждение более слабое, потому что я сразу предположил необходимость взять более сильную теорию множеств. Т.е. теорема П. Фрейда говорит о том, что для универсума гротендика U нет вложения U-малого hTop в U-малый Set. Но это не значит, что нет вложения в Set.

Мне кажется, там проблема не в малости. Фрейд (и покойная? Трнова) доказали кучу теорем, о ограничениях унивалентных вложений.

Там ограничения "алгебраические".

> I don't think that any such example exists, and for good reason. The failure of concretizability is a subtle phenomenon that has nothing to do with abstract algebraic ideas and is instead entirely about size issues (that is, the distinction between sets and proper classes).

To illustrate this last point, if you ignore size issues, then every category is concretizable. Given a category C, you can get a faithful functor to sets by sending each object a to the set F(a) of all morphisms to a. Given a morphism a→b, you get a map F(a)→F(b) by taking any morphism to a and just composing it with the morphism a→b. (Note that this construction is exactly the generalization of the usual proof of Cayley's theorem on groups to general categories.)

Now, this doesn't actually work in general if C is a large category, since the "set" F(a) of all morphisms to a may actually be a proper class. But this does show that any small category is concretizable, and any failure of concretizability has to be about size issues. In other words, it has nothing do with sets and their structure per se (any category would be concretizable if you were allowed to use sufficiently large "sets"). Rather, it must have to do with the structure of the category being in some sense "too large" to embed in the category of small sets.

О, я дошёл до "Given a category C, you can get a faithful functor to sets by sending each object a to the set F(a) of all morphisms to a", а потом подвис. Если бы не стал гуглить, наверное, дотупил бы до доказательства :)

Функтор F, который строят в stackoverflow, не обязательно унивалентный.

Почему? Если F(f) = F(g), то это значит, что для любого объекта a и морфизма h:c→a h.f=h.g, так? Возьмём в качестве h id и получим, что f=g

кто-то енкодил Категорию Гротендика? (agda, coq, idris, etc)

https://wiki2.org/en/Grothendieck_category

🥑Внимание тупой вопрос.
Бывает ли категория (подожди-подожди) натуральных преобразований?

Конечно

Спс, теперь я всё понял!

Это предпорядки какие-то)

Да, точно, я неправильно прочитал определение. Это будет вложение в достаточно большую Set.

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

https://ncatlab.org/nlab/show/arrow+category

Оке, спс)

Чёрт, а есть какой нибудь термин для обобщённого например моноида , чтобы отличать его от обычного моноида из общей алгебры?

Мол читаю википедию "В моноидальной категории можно дать определение моноида, обобщающее свойства моноида из общей алгебры. На самом деле, обычные моноиды — это моноиды в категории множеств с прямым произведением в качестве моноидального произведения."

тут говориться про то что есть два разных моноида.
Понимать про какой имееться ввиду в текстах нужно только по контексту? Или может есть термин, ХЗ