Oℕ
почему нужны естественные, имелось в виду
Size: a a a
2019 June 17
Oℕ
как это говорится, rationale behind
KV
как это говорится, rationale behind
Ну, в общем, с точки зрения пруф-релевантности, естественность гарантирует "естественные" пруф-термы. Например, что коммутативность будет иметь вид
iso (x,y) = (y,x), а не абы какойKV
Остаётся непонятным, зачем, в свою очередь, нужно это, но тут я уже теряюсь абсолютно, да и не особенно интересно
2019 June 18
Oℕ
С точки зрения вычислений, естественность порождает похожие моноидальные законы для процессов
f (×) id¹ ≈ id¹ (×) f ≈ f и
(f (×) g) (×) h ≈ f (×) (g (×) h),
где ≈ - равенство с точностью до композиции со структурными изоморфизмами, дающий рассматривать как бы любой поток вычислений как пучок(список) параллельных элементарных или последовательных подпроцессов
f (×) id¹ ≈ id¹ (×) f ≈ f и
(f (×) g) (×) h ≈ f (×) (g (×) h),
где ≈ - равенство с точностью до композиции со структурными изоморфизмами, дающий рассматривать как бы любой поток вычислений как пучок(список) параллельных элементарных или последовательных подпроцессов
2019 June 19
R:
Хай, что такое категория в теории категорий?
KV
Хай, что такое категория в теории категорий?
Категория в теории категорий - это объект в категории категорий
R:
Категория в теории категорий - это объект в категории категорий
Да, примерно по этому я и спрашиваю
R:
Потому что ничего не понятно
R:
Не все так просто, потому что тогда бы не было смысла разграничивать объект и катеорию как понятия
KV
Если вопрос про определение, то определить можно либо просто как теорию с подходящими символами и аксиомами, либо погрузить в какую-нибудь теорию множеств типа BNF или что-нибудь ещё с классами
NI
Это такой объект, обладающий определёнными свойствами, которые можно отождествить с определением категории.
Смотреть термин "internal category", например —
https://ncatlab.org/nlab/show/internal+category
Смотреть термин "internal category", например —
https://ncatlab.org/nlab/show/internal+category
KV
Не все так просто, потому что тогда бы не было смысла разграничивать объект и катеорию как понятия
Не всякий объект - категория
R:
Началось
NI
Вот есть какая-то категория С.
Как нам описать понятие категории, пользуясь стрелками категории C?
Как нам описать понятие категории, пользуясь стрелками категории C?
KV
Началось
Какой вопрос, такой ответ
Oℕ
Не всякий объект - категория
ой да ладно, всякий же
Oℕ
тривиальную структуру всегда можно доопределить
KV
Oℕ
не всегда можно определить дискретную категорию поверх какого-то класса?