Ну точнее x = x

как Path A x x и т.п.

Т.е. это всё-таки просто пулбек, никакой не волшебный

Если под просто пулбэком подразумевать infty-пулбэк, то да

В HoTT все пулбэки infty, так что если мы работаем в ней, то обычный

И если в нашей категории равенства между морфизмами - это просто теормножественные равенства, то ничего интересного в этом лупспейсе нет, так?
А если задана какая-то более сложная система равенств, тогда наш петлевые морфизмы на найденном объекте будут соответствовать "cпособам доказать, что x = x" ?

Ну да, в 1-категории loop space всегда является подобъектом терминального

Соответственно в распетливании мы как бы восстанавливаем бикатегорию (как помог Павел в другом чате), т.е. из объекта восстанавливаем бикатегорию, где биморфизмы будут равенствами между морфизмами

?

Наверное да, но по бикатегориям это не ко мне. Я могу более простой пример привести.

Буду очень рад послушать

Пусть A -- 1-обрезанное пространство (aka 1-тип, aka 1-группоид, это означает, что все пространства путей в нем дискретны). Пусть a -- точка в A. Тогда пространство петель a = a -- это множество. На нем есть естественная структура группы. Теперь вопрос, если у нас есть группа G, можно ли найти пунктированный 1-тип (A,a) такой, что a = a -- это наша G?

Ответ: да, нужно взять распетливание G. Еще его называют классифицирующим пространством G и обозначают BG, а еще пространством Эйленберга-Маклейна и обозначают K(G,1).

Строится оно так: мы берем точку, присоединяем X петель к ней, где X -- число элементов G. В этот момент мы получаем 1-тип, пространство петель которого -- это свободная группа на множестве X. Мы хотим эту свободную группу превратить в нашу группу G, то есть добавить соотношений. Для этого между различными 1-путями мы подклеиваем 2-пути, чтобы отождествить те 1-пути, которые соответствуют равным элементам группы G. В этот момент мы получаем пространство, которое не является 1-типом. Дальше мы просто подклеиваем высшие ячейки, чтобы исправить эту ситуацию. На языке теории типов последний шаг -- это просто 1-обрезание получившегося типа.

Кстати, я хочу еще отметить важный момент, что delooping строится не просто по объекту/пространству. Например, в примере выше нам важно было не только множество X, но и структура группы на нем. Delooping строится как раз по group object.

Т.к. на loop space есть естественная структура группы, то delooping X -- это объект BX такой, что Loop(BX) эквивалентно X. И эквивалентность здесь подразумевается групповых объектов.

Угу, класс

В другом чате Павел говорил даже про ещё более общий случай делупинга моноидальной категории

Получается, т.к. мы сконструировали только один объект, и никакого единичного объекта нет, внутрь него мы пока залезть не можем.

Это такой совсем свободный какой-то условный объект