Oℕ
Судя по описанию в нкатлабе гомотопический пулбек не сильно отличается от обычного.
С поправкой на то, что "равенства" - это элементы той же (infty, 1) категории
С поправкой на то, что "равенства" - это элементы той же (infty, 1) категории
Size: a a a
2018 November 02
Oℕ
Т.е. если наша категория - это типы и функции. То пространство петель - это как обычный тип Path A x y, для выбранных термов x и y типа A
Oℕ
Ну и теперь, если это корректно, дальше распетливание.
Как это можно осмыслить, что для какого-то типа мы ищем некий "базовый тип", для которого заданный является типом равенства для какой-то пары термов?
Как это можно осмыслить, что для какого-то типа мы ищем некий "базовый тип", для которого заданный является типом равенства для какой-то пары термов?
P
Категорное пространство петель как-то связано с топологическим?
Oℕ
Категорное пространство петель как-то связано с топологическим?
дааа
Oℕ
Категорное пространство петель как-то связано с топологическим?
и распетливание тоже
P
А можешь ссылку на описание категории скинуть?
Oℕ
А можешь ссылку на описание категории скинуть?
категории со слабыми равенствами?
Oℕ
или определение петель/распетливания?
P
категории со слабыми равенствами?
Я про категорное пространство петель спрашивал, но что такое категория со слабыми равенствами я тоже хз :D
P
loop category ничего не выдает в nlab
Oℕ
А это потому что запрос неверный.
Мы не ищем категорию, мы ищем специальный объект https://ncatlab.org/nlab/show/loop+space+object
Мы не ищем категорию, мы ищем специальный объект https://ncatlab.org/nlab/show/loop+space+object
Oℕ
И loop space и delooping - это специальные объекты в категории
Oℕ
V
Вот категорное пространство петель, это как обычный пулбек, мы выбираем пару конкретных морфизмов * -> A?
Пространство петель определяется для пунктирных объектов. То есть у нас есть A и одна точка * -> A, и пространство петель -- это пулбэк этого морфизма ч самим собой.
Oℕ
Пространство петель определяется для пунктирных объектов. То есть у нас есть A и одна точка * -> A, и пространство петель -- это пулбэк этого морфизма ч самим собой.
Т.е. один морфизм всё-таки задан
V
Ну и теперь, если это корректно, дальше распетливание.
Как это можно осмыслить, что для какого-то типа мы ищем некий "базовый тип", для которого заданный является типом равенства для какой-то пары термов?
Как это можно осмыслить, что для какого-то типа мы ищем некий "базовый тип", для которого заданный является типом равенства для какой-то пары термов?
Ну да, delooping -- просто обратная операция.
Oℕ
По-деревенски, задан элемент х: A, мы ищеv что-то типа
Rel A x x
Rel A x x
V
Т.е. один морфизм всё-таки задан
Да, но один, а не два