ЕО
но вот зато в directed type theory...
directed это когда у нас (inf,1)-категории, не группоиды?
Size: a a a
2018 February 23
AG
да, что-то такое, я глубоко не вникал :)
AG
2-топосы там какие то
Oℕ
What homotopy type theory is for homotopy theory/(∞,1)-category theory, directed homotopy type theory is (or should be) for directed homotopy theory/(∞,n)-category theory.
AG
ну идея да, что категории вместо группоидов
Oℕ
One candidate for full omega-categories i.e. (∞,?)-categories? is opetopic type theory.
ЗП
ну еще же есть ctt
AG
про операды писали еще где-то что они там пригодятся
AG
ctt в смысле кюбикал?
AG
так это конструктивная разновидность hott
ЗП
которая вроде более менее заполняет пространство правильно
2018 February 24
ЕО
What homotopy type theory is for homotopy theory/(∞,1)-category theory, directed homotopy type theory is (or should be) for directed homotopy theory/(∞,n)-category theory.
Непонятно только какое они n берут. А если произвольное, то как это всё вместе уживается, ведь не существует никаких (inf,inf) категорий
Oℕ
ну еще же есть ctt
она не сильнее хотт, просто позволят компилить её в голанг
ЗП
она не сильнее хотт, просто позволят компилить её в голанг
?)
Oℕ
ну Алекс говорит, что есть некая ещё более бесконечная хрень, которая позволяет ещё лучше выводить какие-то там равенства
Oℕ
А ты говоришь про низкоуровневую штуку, которая позволяет унивалентность вычислить
ЗП
глобулярно!
Oℕ
глобулярно!
?)
ЗП
ну глобулы