NK
там же проблема с дефинициональном равенстве которое ты не запретил (и не запретишь)
Size: a a a
2017 November 21
TN
ну в ядре тайпечекера (на самом деле там гетерогенный PathP)
TN
где же он обычно определяется
NK
Нужен линейный рефл, т.е. Path a (clone a)
AK
Угу. Поэтому твоё определение — это определение не произвольного n-группоида, а такого, который можно реализовать в виде типа в твоём языке.
TN
ну модификация рефла в ядре
AK
А почему считается, что любой группоид является представленным?
NK
думаю в статье надо смотреть
AK
Ну то есть если мы берём только представленные группоиды, как у вас сделано, то когерентность берётся именно оттуда, что у вас вселенная когерентная. 😊
TN
Я говорил что у нас все просто!
AK
Но это точно такой же читинг, как если бы вы вместо стандартного определения категорий, где бывает произвольный тип объектов Ob и произвольный тип морфизмов Hom[a b : Ob] сразу требовали, чтобы у вас объекты всегда были типами Ob = U, а морфизмы принудительно были всегда Hom[a b : Ob] === (a -> b).
AK
Разумеется, при таком определении окажется, что категория кобордизмов вообще не является категорией.
AK
Ну или является, но только не по определению, а в результате муторнейшего доказательства.
TN
Ага, ты хочешь категорную модель инфинити-групоидов.
AK
Разумеется. 😊
NK
Тут небольшой оффтоп, но может кому будет интересно. А вот есть аналоги System F, в которых параметричность интернализована? Т.е. бесплатные теоремы выводимы? Вроде какие-то работы есть но непонятно докуда они дошли (например есть ли аналог параметричности в MLTT)
TN
Ну мы как все уважающие себя типовыте теоретики в большинстве случаев сразу стриаем структуры, нас интересуют стертые категории, а меня лично, так вообще, стертые типы, и экстракты.
TN
Стурктуралист у нас был Паша :-)
AK
ID:402926333
Тут небольшой оффтоп, но может кому будет интересно. А вот есть аналоги System F, в которых параметричность интернализована? Т.е. бесплатные теоремы выводимы? Вроде какие-то работы есть но непонятно докуда они дошли (например есть ли аналог параметричности в MLTT)
В System F это не имеет смысла, там всё равно ничего доказать нельзя. Я для завтипов есть такие игрушечные системы типов, и там теория развита неплохо.
NK
Я так понимаю что унивалентность нам нагадила и стираемость пропсов пропала (т.е. может что-то и можно стереть но нет понимания что можно а что низя)