VS
С брагилевским так и не получилось? =(((
Size: a a a
2017 November 18
VK
К сожалению.
VK
Ребята сейчас в Минске, все разрулим
2017 November 19
NK
привет! ты то нам и нужен :)
TN
ахаха
AK
Я этто. Пока просто пришёл посмотреть, что у вас тут и как. А то интересно же. 😊
NK
В-общем есть HoTT есть модель HoTT а есть имплементация этой модели на хаскеле (в виде парсера-чекера довольно сырого)
AK
В HoTT модель HoTT? А как вы решили проблему когерентности? (aka определить семисимплициальные типы)
AK
Исаев со временем, наверное, тоже будет. 😊
NK
модель не в хотт а сама по себе, макс дай ссылку на пейпер
NK
Помимо этого есть доказательство что в этой кубической системе индуктивные типы не нужны как примитив, ну или хотя бы не нужны как примитив для "обычных" индуктивных типов, не HiTT
AK
Проблема когерентности, конечно, решается, если в систему добавить хоть самые слабые рудименты принудительного дефиниционального равенства. Это мы знаем.
TN
NK
Док-во в виде дисера, который я в гитхабе формализую в этой кубикал tt. Максим тоже формализует, но пока моих коммитов больше :)
AK
Этот пейпер (1611.02108) я знаю. Хочу, кстати, взять и проработать его с кем-нибудь подробно.
NK
Ну мы сами ничего не решаем, мы сели на плечи гигантов
AK
Ага, эту штуку я читал и как раз очень интересуюсь одной идеей по её части.
NK
Ну базовая либа это отдельный подпроект