TN
ну то, что ты доказывая теоремы рисуешь линии в голове
Size: a a a
2017 November 24
TN
связываешь объекты просто
TN
а в Coq ты переборы индуктивные пишешь ката-ана по деревьям
NK
Ну вот в HoTT этого рисования меньше, другие примитивы
TN
те же
TN
Path индукция
NK
там если очень грубо то эта решетка на отразках заменена на J, он же path-индукция
NK
ну и мортберг говорит что решетка лучше
TN
ну можно да, ввести J и все к нему свести, но будет как бы не очень понятно что внутри
NK
а меня пока не убедил :)
TN
а когда вводишь лямбду на отрезке тогда показано все что скрыто
TN
и J сразу понятно как на атомы разложить
TN
вообщем \(i: I) -> T — это сила!
TN
это и есть суть кубика
NK
ну когда в школе уголком делить учат, про hereditary sets не говорят!
TN
I^n
TN
гомотопический прувинг
TN
отсюда и название cubical
TN
отрезок в степени, гиперкубы
NK
ну ты посмотри на хоттбук.. вот в хотбуке гомотопический прувинг. А в кубике же кубический, на Kan cubical sets