AG
в виде прототипов
Size: a a a
2019 October 08
AG
были задумки его в идрис вмержить но пока добровольцев не нашлось
NI
А он где-то есть?
EPIGRAM, EPIGRAM2 ;-)
ЕО
Кстати интересно с чем удобнее работать для работы с классическими категориями — с OTT или с кубическими типами?
AG
по идее в отт проще
V
ну для 1-категорий и отт хватит
Но там же остаются все проблемы, что и в обычной теории типов, да и в любой конструктивной математике. Чем отт тут помогает?
AG
без сетоидов писать :)
V
Ну это проблемы с конструктивизмом не решает
V
Плюс isomorphism invariance не будет в отт
V
Так что с тем, что там будет проще, можно поспорить
ЕО
"Проблемы с конструктивизмом" это вообще ортогонально, в HoTT те же самые проблемы, proof theoretic strength-то не увеличивается никак
A
Извините за оффтоп, мы в Петербурге собираем кружок по теории категорий, вдруг кому интересно:
https://t.me/joinchat/DrUT-xNs4SJJlfSZv38GPA
Санкт-Петербург, семинары по теории категорий.
Ходить будем по субботам, помещение обговариваем, регламент в данный момент обсуждается в группе.
https://t.me/joinchat/DrUT-xNs4SJJlfSZv38GPA
NI
Извините за оффтоп, мы в Петербурге собираем кружок по теории категорий, вдруг кому интересно:
https://t.me/joinchat/DrUT-xNs4SJJlfSZv38GPA
Санкт-Петербург, семинары по теории категорий.
Ходить будем по субботам, помещение обговариваем, регламент в данный момент обсуждается в группе.
https://t.me/joinchat/DrUT-xNs4SJJlfSZv38GPA
Я думаю, что это не оффтоп.
V
"Проблемы с конструктивизмом" это вообще ортогонально, в HoTT те же самые проблемы, proof theoretic strength-то не увеличивается никак
Не ортогонально. Есть примеры утверждений, которые при обычном определении категорий требуют аксиому выбора, а при унивалентном нет.
ЕО
Не ортогонально. Есть примеры утверждений, которые при обычном определении категорий требуют аксиому выбора, а при унивалентном нет.
А примеры можно таких утверждений?
V
А примеры можно таких утверждений?
Любой полный, строгий, существенно сюръективный на объектах функтор является эквивалентностью категорий.
V
Есть целое отдельное понятие, которое эту проблему позволяет обойти вроде как. Называется анафунктор. На ncatlab подробнее про это есть.
V
Для унивалентных категорий ничего такого не нужно, так как это верно и для обычного определиния функтора и без аксиомы выбора.
ЕО
Любой полный, строгий, существенно сюръективный на объектах функтор является эквивалентностью категорий.
ЕО
Нашёл про это :)