В классическом варианте это, наверное, вообще не сделать: классы просто не формируют никакой категории, мы не сможем internally выбрать Set.

Но можно рассматривать enriched лемму Йонеды internally в какой-то категории.

Не обязательно именно строго внутренне, можно и по Reedy-подобному.

Это как?

"Inner category", это конкретный способ построения.
А они могут быть и другими.
Например, индуктивные типы.
А Reedy-категория, это в которой индуктивные типы могут описывать такие же категории, как и она сама —
https://ncatlab.org/nlab/show/Reedy+category

Не очень понятно как такая штука поможет нам выбрать Set internally 🤔

Или ты о чём?

Она может описать Set внутри чего-то-там...

Если есть желающие дать краткое письменное интервью по тк для европейского научно-популярного блога - пишите в личку. Публикация и перевод бесплатны

Не понял как сделать аналог Set в такой штуке. Я задумался над тем как сделать ngb-подобную категорию, получается как-то так:
1. Нужно взять категорию C, в ней failfull подкатегорию S и эмбеддинг E
2. Нужно чтобы для любого функтора (F: X->S) . (E: S->C) существовал предел. Предел E будет классом всех множеств
3? Нужно как-то сформулировать такое свойство NGB, что все объекты, не являющиеся множествами, изоморфны классу всех множеств. Но тут подумать нужно

Не существование универсума ли это?

Не всякий универсум ведёт себя как класс всех множеств. Интересно как 3'ее свойство на категорном языке сформулировать

Видимо, я не понимаю задачи.
Хочется сделать категорное описание NBG-подобной теории множеств?

Ага, я задался вопросом как такую структуру построить, максимально абстрактно при чём, не хочется сразу требовать топоса

А претопоса можно требовать?

Ещё графическое исчисление про регулярную логику —
https://golem.ph.utexas.edu/category/2019/08/graphical_regular_logic.html
Они же ссылаются на
https://arxiv.org/abs/1812.05765
Ну и наверное, это вот самое примитивное начало, с которого можно начинать говорить про "реляционное" и его обобщения.
#paper

Про старое доброе —
On the dependent product in toposes
Olivia Caramello, Riccardo Zanfa
https://arxiv.org/abs/1908.08488
We give an explicit construction of the dependent product in an elementary topos, and a site-theoretic description for it in the case of a Grothendieck topos.
#paper

недавно узнал что регулярная логика соответствует conjunctive query calculus в бд

Не удивлён. Вот бы оказалось, чтоб претопосы чему-то-там соответствуют, было бы интереснее ;-)

Regular Categories and Regular Logic
Carsten Butz
https://www.brics.dk/LS/98/2/BRICS-LS-98-2.pdf
These notes were supposed to give more detailed information about the relationship between regular categories and regular logic than is contained in Jaap van Oosten’s script on category theory (BRICS Lectures Series LS-95-1). Regular logic is there called coherent logic.
#paper

Всем привет. Начал читать книгу Бартоша Милевски "Теория категорий для программистов".