TN
т.е. ты хочешь импредикативную кодировку в PTS + Path
Size: a a a
2017 November 23
NK
нет, я хочу кубик без индуктивных типов
TN
а ну это получится конечно же
NK
аводи говорит что нет т.к. пропадают HIT
TN
ну HIT не получатся
TN
а просто индуктивные получатся
NK
может они не так и нужны, а может и получится их восстановить
NK
ну Аводи это называет future work
TN
надо просто довести эту работу с кодировками до закрытия гештальта
TN
и сразу в новые глубины
TN
но то что мы счас делаем, оно делается в MLTT (Pi,Sigma) + Path
TN
твой код в coproduct_set.ctt
NK
да, это примерно моя конечная цель и есть
NK
облегчение кубика до состояния в котором индукция ещё не пропала
TN
показания свидетелй совпадают :-)
2017 November 24
NK
кстати интересно что J - это встроенная индукция для Id. Т.е. как бы "остальная индукция реализуема через встроенную для id". Что конечно лучше поскольку пропал фикс
TN
да это мне тоже нравится
TN
с фиксом жить нельзя
TN
а с гомотопическими отрезками одно счастье!
NK
ну мне пока непонятно что в них хорошего, надо войти во вкус