Oℕ
А если бы вообще попытаться абстрактно "категорию" выразить, то тут без завтипов уже совсем анрил
Size: a a a
2018 February 23
Oℕ
Потому что у произвольной категории объектами могут быть не только "типы", но и натуральные числа, и функторы, и вот алгебры. А всё равно нужно тайпчекать, чтобы композиция сходилась
Oℕ
пили на идрисе!
попробую
ЗП
А если бы вообще попытаться абстрактно "категорию" выразить, то тут без завтипов уже совсем анрил
ну вот он тут пытается https://github.com/sjoerdvisscher/data-category
Oℕ
ну вот он тут пытается https://github.com/sjoerdvisscher/data-category
ну вот как я тут выражу категорию натуральных чисел со морфизмом - порядком?
ЗП
ну вот как я тут выражу категорию натуральных чисел со морфизмом - порядком?
делай на агде)
Oℕ
делай на агде)
ну попробую на идрисе
Oℕ
setoid hell
KV
setoid hell
А это реальная проблема?
AG
ну да, для этого и начали сочинять hott-ы всякие
KV
Хм, и правда
AG
правда в hott-е по моему с категориями тоже не всё слава богу, говорят когерентности там муторные
AG
но вот зато в directed type theory...
KV
Оп, ещё один покемон
ЗП
шульман?
AG
и ликата
Oℕ
[0000] days since last googling things mentioned by clayrat
Oℕ
правда в hott-е по моему с категориями тоже не всё слава богу, говорят когерентности там муторные
когерентности - это равенства между морфизмами?
AG
между определенными сочетаниями да