NK
так мало ли чего достаточно
Size: a a a
2017 November 23
TN
так Фикс в корекубике
TN
даже сплиты мы туда добавили
TN
т.е. вообще индуктивные типы
TN
CiC
NK
не мы а вы!
TN
data tele (A: U) = empty | tel: name → A → tele A
data branch (A: U) = br: name → list name → A
data label (A: U) = lab: name → tele A
data O4 = O3
| Sum: name → tele → list (label O4)
| Split: name → list (branch O4)
| Ctor: name → list O4
data branch (A: U) = br: name → list name → A
data label (A: U) = lab: name → tele A
data O4 = O3
| Sum: name → tele → list (label O4)
| Split: name → list (branch O4)
| Ctor: name → list O4
TN
ну можно без этого
TN
тогда чистый ОМ
TN
а-ля
TN
дело техники
NK
вот! и вопрос если встроенных фикса и индукции нету что у нас с унивалентностьб
TN
ААА
NK
ну и вообще HIT же пропадают
TN
ну ты типонавт!
TN
даже я про такое не думал!
NK
так а нахуя я тогда этой кодировкой занимаюсь
NK
это ж единственная цель - почистить коре от фикса и индуктивных типов
TN
во-первых это понятно, знакомо и мы специалисты в этом
во-вторых тренируемся на кубике
во-вторых тренируемся на кубике
NK
и посмотреть не пропадет ли унивалентность, т.е. можно ли ее доказать без использования HIT (которых у нас нет т.к. кодировка не позволяет вылезти за пределы Set)