Oℕ
Size: a a a
2019 June 12
Oℕ
там просто же с хотбука
Oℕ
не могу прочувствовать, какие двери открывает унивалентность
Oℕ
ЗП
ну про унивалентность же
ЗП
еще в вики есть https://wiki2.org/en/Univalent_foundations
Oℕ
Эх зигоморфизм, зигоморфизм
Oℕ
Мы же про кусок опредедения категории говорим
ЗП
ну я в хотт буке тоже это не понял
AG
вот тут вроде расписано про это
https://arxiv.org/abs/1303.0584
Ahrens, Kapulkin, Shulman, "Univalent categories and the Rezk completion"
https://arxiv.org/abs/1303.0584
Ahrens, Kapulkin, Shulman, "Univalent categories and the Rezk completion"
AG
основная идея вроде всё та же что и с обычной унивалентностью - использовать изоморфизмы как равенства
ЗП
основная идея вроде всё та же что и с обычной унивалентностью - использовать изоморфизмы как равенства
ну это понятно
AG
A good example of the difference between the three notions of category is provided by the statement “every fully faithful and essentially surjective functor is an equivalence of categories”, which in classical set-based category theory is equivalent to the axiom of choice.
(i) For strict categories, this is still equivalent to to the axiom of choice.
(ii) For precategories, there is no axiom of choice which can make it true.
(iii) For saturated categories, it is provable without any axiom of choice.
Oℕ
вот тут вроде расписано про это
https://arxiv.org/abs/1303.0584
Ahrens, Kapulkin, Shulman, "Univalent categories and the Rezk completion"
https://arxiv.org/abs/1303.0584
Ahrens, Kapulkin, Shulman, "Univalent categories and the Rezk completion"
о, спасибо
AG
насыщенные это как раз хоттовские категории
Oℕ
A good example of the difference between the three notions of category is provided by the statement “every fully faithful and essentially surjective functor is an equivalence of categories”, which in classical set-based category theory is equivalent to the axiom of choice.
(i) For strict categories, this is still equivalent to to the axiom of choice.
(ii) For precategories, there is no axiom of choice which can make it true.
(iii) For saturated categories, it is provable without any axiom of choice.
ага
Oℕ
прикольно
V
В категориях все универсальные конструкции буквально уникальны. Т.е. любые два начальных объекта буквально равны, любые два произведения равны, два сопряженных функтора к данному равны, и т.д. В предкатегориях они будут только изоморфны.
P
Что такое равенство в категории?