❤️

Для всех существующих определений (\infty,1)-категорий известно, что они эквивалентны.

(\infty,1)-категория моделей гомотопической теории типов эквивалентна (\infty,1)-категории (\infty,1)-категорий с доп. структурой, которая зависит от конструкций, которые мы добавляем в HoTT.

Всё-таки, это слишком сильно сказано.
Надо пояснять, в каком смысле эквивалентны (что отчасти сделано в следующем комменте).
Иначе тут же вопрос — а почему это тогда не используют глобулярные хрени, ведь они проще всего? ;-)

Эта категория как-то соотносится с какими-нибудь категориями мотивов?

Эквивалентны как квазикатегории. Вопрос в том, что я подразумевал под словами "существующие определения (\infty,1)-категорий", так как уже в них скрыто утверждение о том, что это определение корректно, т.е. несколько тавтологичное утверждение получилось.

Нет. Что навело на такую мысль?

Импульсивно задал вопрос, не обдумав хоть чуть ;-)
В смысле, что сам уж понял.

Скажем так, некоторая интуиция возникла, но попытки её обдумать сколько-то строго, что надо было мне сделать до того, как я задал вопрос ;-), приводят к чуши.
Может быть, какие-то мысли получше ещё появятся.

Ну, я могу сказать откуда это берется. Просто я хотел какой-то наводящий вопрос для начала задать, но могу и так рассказать.

Очень любопытно ;-)

Самый простой случай — это категория моделей просто типизированного унарного лямбда исчисления (без типов функций, произведений и прочего). Унарность означает, что контекст у нас всегда состоит ровно из одной переменной. По определению модель этой теории состоит из множества типов, для каждой пары типов A и B множества термов (типа B в контексте x : A), функции, сопоставляющей каждому типу A терм x : A |- x : A и функции подстановки, которая каждой паре термов x : A |- b : B и y : B |- c : C сопоставляет терм x : A |- c[b/y] : C. Эти функции должны удовлетворять следующим свойствам: x[b/x] = b, c[x/x] = c, c[b/y][a/x] = c[b[a/x]/y]. Если приглядеться, то можно заметить, что эти данные в точности соответствуют категории. То есть модели такой теории типов = категории.

Если мы вместо унарной теории типов рассмотрим обычную и добавим тип произведений, то модели такой теории типов будут эквивалентны декартовым категориям. Если мы еще добавим тип функций, то декартово замкнутым.

Если мы перейдем к зависимым типам и добавим сигма-типы и экстенсиональные Id-типы, то модели будут эквивалентны конечно полным категориям. Id-типы здесь примерно соответствуют уравнителям. Если мы еще добавим пи-типы, то получим локально декартово замкнутые категории.

Это результат, который был сформулирован еще Seely, но в его доказательстве была ошибка, и окончательно его доказали где-то в районе 2010, точно не помню.

Теперь, если мы вместо экстенсиональных Id-типов будем рассматривать интенсиональные, то категория моделей будет представлять естественным образом некоторую (\infty,1)-категорию. И она будет эквивалентна (\infty,1)-категории конечно полных (\infty,1)-категорий (если мы берем теорию с сигма-типами и Id-типами). Это доказали где-то год назад Капулкин и Szumilo. Пока это всё, что известно. Насколько я знаю Капулкин сейчас работает над тем, чтобы доказать это для теории с пи-типами и локально декартово замкнутых (\infty,1)-категорий.

А, да, забыл. В низшем случае там не эквивалентнсоть категорий, а биэквивалентность 2-категорий.

А откуда в экстенсиональном случае там "2" берётся?
Статья эта у меня даже есть, но абсолютно про неё забыл... Пасиб!

Объекты — типы, морфизмы между A и B — термы x : A |- b : B, 2-ячейки между b и b' — термы x : A |- p : Id(b,b')