Хочу заметить, что определение через bind можно дать и для произвольных категорий, если аргументы расположить в правильном порядке: bind : Hom(X,TY) -> Hom(TX,TY), где T : C -> C — функтор.

И это определение даже удобнее в каком-то смысле, т.к. нам нужно только проверить монадные законы. Естественность и даже функториальность T получается бесплатно из них.

Т.е. монаду можно определить как функцию T : Ob(C) -> Ob(C) вместе с функциями \eta_X : Hom(X,TX) и bind как описано выше, которые удовлетворяют монадным законам.

Если все ужать по максимуму, то можно увидеть схожесть вот так вот:

Моноид на множестве S:
mult: S x S -> S
id: 1 -> S

Монада (Id - это identity endofunctor, который будет аналогом множества с одним элементом):
join: Maybe о Maybe -> Maybe
return: Id -> Maybe

Народ всем Привет, подскажите самый современный инструмент записи и работы с выражениями теории категорий

Интересная тема) +1 к вопросу. Я вот по-старинке до сих пор - блокнот и ручку использую. Рисовать можно много чего. Если программировать нужно, то можно на языках с завимимыми типами что-то пробовать делать.

Струнные диаграммы?

Может быть есть вариант взять какойто нормальный DSL заточенный под теорию категорий, держать например базу в виде таблицы связей, гонять некие агенты итд

Я думал для таких целей Coq используют.

А он всё переваривает ? Вот например доказать комутативность магмы там можно ?

Есть библиотеки, которые описывают теорию категорий

Например https://github.com/jwiegley/category-theory

Тернарные полугруппы, тема прикольная. Композиция стрелок асоцитивна в ТК. Прикиньте тернарная асоциативность.

[Open Mathematics] Ternary and n-ary f-distributive structures.pdf

В универе я работы в техе писал...

Ну ТеХ это понятно, но думаю, что слишком уж накладно, если сравнивать с диаграмамми (струнными, коммутативными) в блокноте. Наверное, ничего более современного и автоматического в сравнении с зав типами (cubicaltt например) и нету.

Бывает и n-арная.
Для моноидального произведения "unbiased monoidal category" называется, хотя и по сути, просто другая форму бираной ассоциативности.
А в мультикатегориях и n-категориях, развивают всякое-всякое...

Всем привет. Я так понял, тут должны быть математики (у меня нет профильного образования), чтобы уточнить один момент, связанный с алгебраическими структурами.

http://math.chapman.edu/~jipsen/structures/doku.php/semirings -  в этом источнике утверждается, что полукольца - это полугруппы (то есть, без единичных элементов для сложения и умножения). Для единичных элементов структуры имеют немного другое название:
http://math.chapman.edu/~jipsen/structures/doku.php/semirings_with_identity
http://math.chapman.edu/~jipsen/structures/doku.php/semirings_with_zero

https://en.wikipedia.org/wiki/Semiring - в Википедии же утверждается, что полукольца есть моноиды.

Кому верить? 🤔