AZ
по-моему правило композиции одно для всех категория: если есть a -> b и b -> c, то можно сделать a -> c = f * g
Size: a a a
2019 August 27
YS
просто что такое "правила композиции" мне не совсем понятно
задайте композицию, как вы на предыдущем шаге задавали ассоциативную операцию для моноида
SM
по-моему правило композиции одно для всех категория: если есть a -> b и b -> c, то можно сделать a -> c = f * g
Но ведь могут быть разные стрелки из a в c
SM
Какая из них собственно будет композицией?
AZ
SK
1 о 0 = 1 для ||
1 о 0 = 0 для &&
композиция разная
1 о 0 = 0 для &&
композиция разная
AZ
"Monoid as a catagory" — это один объект со стрелками, причём в объекте как бы лежат элементы моноида, в данном случае, True и False. В моноиде-как-категории натуральных чисел операцией будет арифметическое сложение, а морфизмы будут вида
\x -> x + y для всех y из натуральных. Соответственно, тут будет \x -> x && True и \x -> x && FalseНу вот человек написал. Первое это id для && и второе это not, а для || наоборот
YS
по-моему правило композиции одно для всех категория: если есть a -> b и b -> c, то можно сделать a -> c = f * g
нет, здесь вы только утверждаете, что композиция возможна. а теперь надо задать её.
KV
Ну вот человек написал. Первое это id для && и второе это not, а для || наоборот
Это не
notЕО
по-моему правило композиции одно для всех категория: если есть a -> b и b -> c, то можно сделать a -> c = f * g
Это не правило композиции, это "тип" композиции. А правило это то как композиция задаётся, уравнения вида
x . y = z, для всех x : A->B и y: B->C
x . y = z, для всех x : A->B и y: B->C
KV
Там
id и const False получаетсяSK
@Это не
да
notда
SK
там два const’a 🙂
ЕО
Но вообще непонятно чего вы тут программирование какое-то развели
KV
Ещё раз: в моноиде-как-категории мы берём все
y из моноида и составляем стрелки вида \x -> x * y. Вот они-то и есть морфизмы категорииЕО
Тут про теорию категорию вроде, а не про идрис :)
SK
хах, упражнения Бартоша же
IJ
по-моему правило композиции одно для всех категория: если есть a -> b и b -> c, то можно сделать a -> c = f * g
в моноиде две "интересные" стрелки:
(and False) и id, надо просто выписать, чему равны их композиции.NI
в моноиде две "интересные" стрелки:
(and False) и id, надо просто выписать, чему равны их композиции.Ну и показать, что они получились ассоциативными и с единицей ;-)
YS
"Monoid as a catagory" — это один объект со стрелками, причём в объекте как бы лежат элементы моноида, в данном случае, True и False. В моноиде-как-категории натуральных чисел операцией будет арифметическое сложение, а морфизмы будут вида
\x -> x + y для всех y из натуральных. Соответственно, тут будет \x -> x && True и \x -> x && False1. что такое "как бы лежат"?
2. но это же будет изоморфно более простой категории: взять что угодно за единственный объект, элементы за стрелки и их операцию за композицию
2. но это же будет изоморфно более простой категории: взять что угодно за единственный объект, элементы за стрелки и их операцию за композицию