PS
а зачем? категории конструктивны, вся базовая теория категорий доказывается на обычном ML
Size: a a a
2019 April 10
NI
а зачем? категории конструктивны, вся базовая теория категорий доказывается на обычном ML
https://ncatlab.org/nlab/show/anafunctor
Прочитайте самое начало, пожалуйста.
Прочитайте самое начало, пожалуйста.
Oℕ
а зачем? категории конструктивны, вся базовая теория категорий доказывается на обычном ML
Очень много бойлерплейта обычно уходит на ассоциативность, например и реврайты с субпоследователтностями морфизмов, равных, например айдентити
Oℕ
Наверняка есть конечно что-то равносильное коммутативным диаграммам, но теперь не найду
PS
https://ncatlab.org/nlab/show/anafunctor
Прочитайте самое начало, пожалуйста.
Прочитайте самое начало, пожалуйста.
прочитал
NI
прочитал
Я к тому, что "категории конструктивны" надо уточнять.
Это не совсем так.
Это не совсем так.
Oℕ
А если хомсеты там сетоиды, и вовсе беда
PS
Очень много бойлерплейта обычно уходит на ассоциативность, например и реврайты с субпоследователтностями морфизмов, равных, например айдентити
PS
Я к тому, что "категории конструктивны" надо уточнять.
Это не совсем так.
Это не совсем так.
а можно пример теоретико-категориального утверждения, доказываемого неконструктивно? мне интересно
CE
Всякий стафф с построением левых/правых сопряженных
CE
По универсальным стрелкам
CE
Аксиому выбора приходится задействовать
CE
Собственно анафункторы помогают с этим что-то делать
Oℕ
Угу. Ну вот я в аренде тоже через ХоТТ делал.
Вот как раз яркий пример.
https://github.com/pcapriotti/agda-categories/blob/master/category/trans/ops.agda#L36
То, что должно доказываться в одно-два действия превращается в кучу ассоциативностей и частных переписываний равенств
Вот как раз яркий пример.
https://github.com/pcapriotti/agda-categories/blob/master/category/trans/ops.agda#L36
То, что должно доказываться в одно-два действия превращается в кучу ассоциативностей и частных переписываний равенств
Oℕ
Если что-то более интересное, там само доказательство вообще теряется на фоне ассоциативностей и базовых действий с равенствами
Oℕ
Хотя кажется, что многие штуки конкретно с хомсетами можно эффективнее автоматизировать
Oℕ
Но в аренде нет совсем тактик.
В идрисе вроде элаборейшон, но я совсем ещё мало умею и в идрисе же К, поэтому, как я понимаю всё через сетоиды придётся
В идрисе вроде элаборейшон, но я совсем ещё мало умею и в идрисе же К, поэтому, как я понимаю всё через сетоиды придётся
CE
а можно пример теоретико-категориального утверждения, доказываемого неконструктивно? мне интересно
Еще есть известный неконструктивный факт: любая малая полная категория является порядковой(хом множества самое большое одноэлементные)
CE
Интересно, это в хотте доказуемо?
PS
Еще есть известный неконструктивный факт: любая малая полная категория является порядковой(хом множества самое большое одноэлементные)
ух ты. а можно меня ткнуть в существующее доказательство этого факта?