а линал закончился на "ну эт матрица ребята"

Логику предикатов?

теории первого порядка

ну и пеано

А, ну тогда всё просто. Когда он пишет про стрелки и объекты, он всего-лишь имеет в виду переменные особого вида

Ну и мыслите себе теорию категорий как формальную теорию. Только сильно не надо особо вдумываться в детали формализации

Типа у нас есть язык, в котором есть переменные A, B, C, ... и f, g, h, есть константа id, функциональные символы dom и cod, предикат бинарный = и дальше аксиомы

во, уже лучше)

спасибо

ладно, надо работать)

Надо ещё два унарных предиката добавить — является ли стрелкой и является ли объектом :)

а ссылку на алгебраический чат можно?

https://t.me/ru_abstract_algebra но он немного мёртвый (недостаток алгебраистов сказывается)

На теории категорий и без участия ZFC/NBG можно и теорию множеств построить.

Интересно — а higher category можно?

Довольно-таки уверен, что можно.
Хотя и именно в таком виде, не видел таких попыток...
Те же гомотопические типы, это один из вариантов (∞,1) и есть.
И видимо, можно переформулировать и n-категорно...
Более-менее очевидно, что можно и (∞,n) сделать.
Например, опетопами. Или клеточными множествами (диски Joyal'а).

Я спрашивал про попытки. Понятно, что так-то можно на языке higher category theory сформулировать язык теории (малых) множеств, а дальше просто зафиксировать необходимые и достаточные свойства в качестве аксиом :)

Про гомотопическую теорию типов интересно насколько она эквивалетна существующим определениям (inf,1)-категорий

Я так понимаю там же зоопарк полный с определениями

Ну вот что с нуля сделано, оно ж так и строится.
В смысле, что взяли какую-нибудь из конструкций кубов, посмотрели для них критерий фибрантности, попытались сделать конструктивное определение.
Т.е., если там несоответствия и могут быть, то где-то на уровне максимум "Hask — не категория".
Или для симплексов "комплексы Кана" (по понятным причинам, исторически первая испробованная кнструкция).
Впрочем, я тут не уверен... Может быть, первая испробованная конструкция была таки на основе глобулярных множеств, просто по причине простоты констуркции.