За прошедшие с тех пор 11 лет, в области произошло несколько впечатляющих и вдохновляющих прорывов, но центральная задача — создания синтетического языка для ∞-группоидов, достаточно выразительного, чтобы прямо в нем можно было формулировать все математические идеи — пока остается открыта. Предложенный язык интерпретируется в категориии ∞-группоидов (равно как и во всех остальных ∞-топосах Гротендика!) и в нем можно записать довольно много математики (и это активно делается, каждый месяц выходят статьи на нем), но мы пока не знаем, например, можно ли в нем собственно определить понятие категории (в общем смысле этого слова, т.е. когда Ob, Mor — ∞-группоиды, а не множества).

Поэтому мы пока продолжаем использовать несколько неестественный и неуклюжий, но (после быстрого обретения точных интуиций и опыта) не мешающий думать и следовать принципу эквивалентности set-based язык.

Касательно терминов, сейчас вместе с «∞-группоидом», синонимично используют слова: «анима», «гомотопический тип», «тип». Мне видится наиболее удачным последнее — оно точнее всего отражает дух этого понятия, как базового концепта, близко к его классическому частному случаю — «множеству», поэтому я использую его (а n-группоиды называются соответственно n-усеченными типами или n-типами).

«Анима» было намеренно придумано Шольце-Клаузеном (их мотивация совершенно естественна и в точности совпадает с моей, но интересно почему они просто не использовали «тип», учитывая, что в этот момент HoTT уже давно освещал мир?), а «гомотопический тип» возникает из того, что согласно гомотопической гипотезе Гротендика, типы — это и есть предмет изучения классической теории гомотопий. А именно, естественный функтор

Top → Type, пространство отправляется в тип, Ob, которого — точки пространства, Isom — пути в пространстве, 2-Isom — гомотопии путей, 3-Isom — гомотопии гомотопий etc

переводит слабые эквивалентности топ. пространств (отображения, индуцирующие изоморфизмы на всех гомотопических группах со всеми отмеченными точками и биекцию на pi_0) в изоморфизмы и индуцированный функтор из локализации Top[W^{-1}] → Type эквивалентность категорий.

Собственно ещё один, идущий отсюда, (но во всех отношениях неадекватный) термин-синоним — «пространства» 🤯 — был почему-то популяризован Лури и поэтому в данный момент все ещё используется массово. Но, конечно, как видно из слов Шольце по ссылке выше и многих математиков, начиная с первого сообщения Урса, здесь, сообщество старается уйти от него.

—

Интуитивно о типах, во-первых, полезно думать как о множествах: для них определены все те же самые понятия и конструкции, к которым вы привыкли в категории множеств (а также все их старшие версии) и, более того, продолжают выполняться все утверждения («более того»? — типовая/структурная точка зрения как раз стирает разницу между понятием и утверждением, как вы могли начать замечать). В том смысле, что некоторые претерпевают естественную когерентную модификацию, то есть в некоторых формулировках происходит обнаружение скрытого числа «1» и немедленная замена его на «∞».

Иллюстрируя множественные интуиции:

* Cюръекией типов называется функция f: A → B т.ч. для каждого b : B просто существует a : A т.ч. f(a) = b (последнее выражение значит, конечно, просто существует a: A и p: f(a) = b).

* Вложением (или инъекций) типов называется функция f: A → B т.ч. для каждых a, a' : A, отображение a = a' → f(a) = f(a') изоморфизм.

Смысл второго понятия: мы в точности выбираем часть объектов -- они остаются с тем же устройством равенства, которое было. Концепт подтипа.

Здесь пока не определялось формально, что такое типы и их функции, но мы знаем это для 1-типов — группоидов и для них можем понять эти определения буквально.

Имеет место

Теорема.
* f: A → B изоморфизм типов <=> f инъекция и сюръекция
* Каждая f: A → B канонически раскладывается как композиция cюръекции и вложения A → im f → B.

Упр. Докажите теорему для 1-типов.