NK
а у меня ещё детское время
Size: a a a
2017 November 21
AK
А, не, пока дочь решила есть, так что ещё попишу.
TN
в тексте я так понял про комоноидальные, дуальные категории речь идет
NK
в посте кстати упоминался LinHoTT
AK
Ну да. Виртуальный и не придуманный ещё. 😊
TN
Институт Времени (тм)
AK
В общем, как раз из алгебраических структур, работающих на квантовых (неклонируемых или клонируемых очень специальным образом) объектах появляется некоторая интуиция, как эта хрень должна работать.
AK
В смысле линейные типы.
AK
Из этой интуиции вытекают следующие соображения:
NK
я так понимаю, проблема в "неразрушающих наблюдениях". Т.е. нам нужен способ формулировать утверждения об объектах, не разрушая их или разрушая но тут же создавая эквивалентные клоны
AG
это в принципе уже сделали Макбрайд/Этки
AK
Угу. И использование объекта не на уровне термов, а на уровне типов — т.е. в качестве "индекса", если угодно, не является разрушающим наблюдением.
AK
Должно получаться, что для всякого линейного типа существует Id-тип, наделённый естественной структурой алгебройда хопфа (линейный аналог группоида), причём Id-типы второго порядка автоматически являются коммутативными и кокоммутативными.
NK
а где они это сделали? просто я отсталый и мне для всего нужны буквари
AG
более того, оно уже есть в идрисе :)
AK
По аналогии, кстати, с https://homotopytypetheory.org/2011/03/26/higher-fundamental-groups-are-abelian/.
AK
Т.е. начиная с третьего порядка, оно "почти интуиционистское".
AK
Кокоммутативное и коассоциативное, но не обязательно коидемпотентное.
NK
но если мы делим использования на разрушающие и неразрушающие, это ж какая-то стратификация появляется, которая "всё портит"?