AK
Да вот вроде как не портит, см. указанную статью.
Size: a a a
2017 November 21
AK
Там всё довольно интересно выходит на уровне категорной семантики в терминах стеков, но я слишком тупой и пока не вкурил.
AG
там какие то семейные категории, я про такое даже не слышал :)
AG
я вот наслышан про моноиды Хопфа как раз в контексте линалга (кинул картинку в камент к посту в жж)
AG
не знал что оно и в линейно-зависимом вылазит
AK
Короче, то что мы ищем на уровне семантики — это линейный аналог инфинити-группоидов в том же смысле, в котором алгебра Хопфа является линейным аналогом группы.
TN
inf_grpd (A: U): U =
(carrier: A)
* (eq: (a b: A) -> Path A a b)
* (next: (a b: A) -> inf_grpd (Path A a b))
* Unit
(carrier: A)
* (eq: (a b: A) -> Path A a b)
* (next: (a b: A) -> inf_grpd (Path A a b))
* Unit
TN
а чем такой инфинити-групоид не линейный ?
NK
то есть это HoTT где вся дупликация явная
AK
Как Воеводский понял, что типы суть абстракция инфинити-группоидов, так и тут должно получиться, что линейный тип суть абстракция этой штуки.
AK
Эм. Как определение инф-группоида, которое ты привёл, даёт нам когерентность?
NK
нелинейный хотя бы тем что все рефлы существуют
AK
ID:402926333
нелинейный хотя бы тем что все рефлы существуют
Ну вот собственно, да. Рефлы тут диагонали.
TN
ну можно написать аксесор который только раз берет eq и сразу на next переходит
NK
т.е. надо J и path induction запретить и те пе, а как их начинаешь запрещать многое вылазит
TN
или какие-то ограничение на сам Path который в eq вы хотите наложить?
AK
А, я понял. Это определение инфинити-группоида представленного типом А. Т.е. просто пользуемся данными свыше свойствами вселенной, чтобы у нас получилось. Ну это читинг. 😊
NK
возвращаясь на низкий уровень - нам в исчислении нужны объекты, у которых нет дефиниционального равенства
NP
Николай, а вы откуда и чем занимаетесь в науке?
Да я магистрант из Киева просто, сейчас во ВШЭ учусь. В Киеве занимался квантовыми деформациями алгебр Кунца и прочей теорией представлений С*-алгебр и квантовых групп, а тут пытаюсь некоммутативной производной алгебраической геометрией в духе Концевича и Собельмана. В типы въезжаю в свободное время в своём темпе :з