Хитрость тут в том, что пока основания классической математики развиваются так: есть довольно небольшой список средств выразительности, которых, как кажется, достаточно для чего угодно, нужно лишь постулировать всё новые и новые способы конструирования линейных порядков (т.н канторова лестница). Старая теория при этом в новой представляется как некое множество маленьких множеств.
Насколько мне известно самым продвинутым способом конструировать порядки, совместимым с аксиомой выбора, является rank-into-rank embedding, а в принципе версия кардинала беркли (что, кстати, основной контраргумент для меня против аксиомы выбора -- без неё можно забраться выше по канторовой лестнице)

http://cantorsattic.info/Rank_into_rank
http://cantorsattic.info/Berkeley

То есть f это +1, g это +2, g * f это +3, и они соовтетсвуют 1,2 и 3 во множестве?

При условии что мы про множество натуральных чисел

читаю книжку, клевая, но мозги немного скрипят

Всё так.

спасибо, иду дальше)

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

Можно и на множестве бесплатно определить моноид, как множество эндо-функций (т.е. x->x).

Во-первых, это моноид, очевидно.
Во-вторых, для любого моноида в обычном смысле, найдётся такое множество, что все преобразования которого будут изоморфны этому моноиду.

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

Для множества натуральных чисел, полагаю, достаточно стрелок id и еще одного морфизма из объекта в объект.

Если определять классически, то без явного задания свойств-равенств моноида, никак не обойтись.

про это, мне кажется, удобнее думать как про множество строчек, составленных из букв g и f с конкатенацией.

мне в числах как-то проще. Хотя строчки тоже валидны офк

Можно определить моноид, порождённый какими-то функциями.
Т.е., как список [x->x] и с композицией.
Ассоциативность будет выполняться автоматически.
Наверное, я не понимаю, в чём вопрос.

наверное я пока не знаю половину ответа чтобы задать нормальный вопрос)

ну вот пример моноида на идрисе

ятп тут ничгео не помешает сделать реализацию которая не будет моноидом