TN
Size: a a a
2017 November 23
TN
типа конкурент Twelf
TN
я помню мы шутили еще что у автора дедукти класная фамилия (Гильберт)
TN
а хотелось бы )
TN
вот кстати тот пейпер Univalence on Dedukti
NK
Мы вместе занимались. Основные работы Аводи по невозможности индукции - это 2012 год.
NK
Ну т.е. он понял что Пашино направление гиблое в районе 2010-го или раньше, надо посмотреть по лит-ре где эти эта-аксиомы описаны
NK
а потом ещё 7 лет ебался как эта-аксиому к кодировке прилепить
NK
ну и конечно это всё предварительно, толком выясним чего в Оме не хватало только когда закончим
NK
(и это всё ещё до алгебр-через-лимиты, поскольку индукции даже у була нет)
NK
проблема почему индукции нет - есть лишние инхабитанты которых надо запрещать, но непонятно как
TN
а про какую статью Эводи ты говоришь? я видел только Гувера про запрет в P2 (безфункторную систему) или забыл
TN
с селф-типами Стампа и Ли индукция сразу выводится
TN
индукция в PTS занимает килобайты, унивалентность в кубике мегабайты
TN
но чтобы в инфините топосе что-то было нельзя сделать, таких статей не может быть )
TN
Коньюнктура Сохацкого: существует кодировка HIT в PTS-\infty
NK
TN
это работа Сояковой
NK
ну собственно аводи там в соавторах и это теор. основа нашей текущей кодировки