TN
ты как-то странно это видишь
Size: a a a
2017 November 24
NK
ну или покажи мне в хоттбуке гиперкубы )
TN
cubical — это просто язык который писали всей бандой для того чтобы учебник HoTT закодировать
TN
сначала пробовали инфинити-групоиды и глобулярную теорию –— соснули
NK
я вижу это так. В HOTT есть какие-то примитивы. Например там, даже cong aka mapOnPath это примитив!
TN
потом Воведовский пробовал симплицидальные множества — треугольники — соснули
TN
потом попробовали кубы — получилось!
TN
то что в HoTT — это уже старье, оно было актуально для предыдущего прувера в репе Гувера
TN
там J mapOnPath и cong именно примитивы
TN
и нет отрезка
NK
да да
TN
потом Исаев хотел сесть на коня из Джет Брейнс и сделал отрезок (его даже Мортберг цитирует)
TN
но не успел до конца
TN
Мортберг сел на коня
TN
и мы за ним!
NK
ну вот в учебнике HoTT устаревшие док-ва на примитивах. Это как в коке устаревшая индукция на встроенных полиномиальных функторах
TN
не такое оно и устревшее если оно на mapOnPath cong и J
TN
это ж современная базовая либа
NK
Ну и моя позиция что может так и надо писать!
TN
но идея твоя понятна!