TN
В моем понимании инфинити-групоид — это стрим. Пока вроде сходится.
Size: a a a
2017 November 21
NK
поскольку оно нелинейно, т.е. a -> Path a a это сразу зашквар
AK
Да я магистрант из Киева просто, сейчас во ВШЭ учусь. В Киеве занимался квантовыми деформациями алгебр Кунца и прочей теорией представлений С*-алгебр и квантовых групп, а тут пытаюсь некоммутативной производной алгебраической геометрией в духе Концевича и Собельмана. В типы въезжаю в свободное время в своём темпе :з
Это прекрасно. У вас как раз наверняка есть какие-то интуиции и подходы к тому, как должны быть устроены линейно-типовые аналоги инфинити-группоидов. 😊
AK
В моем понимании инфинити-групоид — это стрим. Пока вроде сходится.
В моём понимании — инфинити группоид это тоже стрим, только с условиями когерентности.
AK
Т.е. для начала это стрим произвольных типов, индексированных элементами предыдущих типов.
AK
Т.е. он состоит из типа Carrier, типа Path[a b : Carrier], типа Cell[aa bb : Paths[a, b]], Cell2[aaa bbb : Cell[aa, bb]] и так далее.
TN
ну так точно так я и написал :-)
TN
в коиндуктивном типе
TN
теперь надо когерентность добаивть
TN
как?
AK
Э, нет.
Ты написал, что eq сразу живёт в predefined на уровне языка типе Path.
Ты написал, что eq сразу живёт в predefined на уровне языка типе Path.
AK
А я говорю, что для начала у нас есть стрим (сильно-зависимый) типов.
TN
я продолжил всего-лишь n-groupoid
AK
А когерентность потом добавляется аксиомой, что любая замкнутая диаграмма имеет филлер.
TN
mutual
rec (A: U) (a b: A): (k: nat) -> U = split
zero -> Path A a b
succ n -> n_grpd (Path A a b) n
n_grpd (A: U) (n: nat): U = (a b: A) -> ((rec A a b) n)
prop (A: U): U = n_grpd A zero
set (A: U): U = n_grpd A (succ zero)
groupoid (A: U): U = n_grpd A (succ (succ zero))
rec (A: U) (a b: A): (k: nat) -> U = split
zero -> Path A a b
succ n -> n_grpd (Path A a b) n
n_grpd (A: U) (n: nat): U = (a b: A) -> ((rec A a b) n)
prop (A: U): U = n_grpd A zero
set (A: U): U = n_grpd A (succ zero)
groupoid (A: U): U = n_grpd A (succ (succ zero))
TN
если продложить до бесконечности, получится в точности та коиндуктивная структура которую я привел
TN
а эта штука точно n-groupoid так как в нашей либе юзается
TN
это не может быть ошибкой!
AK
У тебя zero принудительно маппится в Path A a b.
AK
Откуда берётся тип Path? Где он определён?