это слишком очевидное решение, думаю @Comonoid о таком не спрашивал бы

оно фактически эквивалетно тому, что я предлагал с высшими индуктивными типами, просто т.к. в хаскеле нет законов и этот замут не нужен

Да, это тут интересным не будет.

Не могу придумать приимер, почему оно не универсальное.
Кажется, что это не так.
Вот если бы  Applicative f был изоморфен Applicative (FreeMon f) ;-)

А как он может быть изоморфен, если фримонада - это строго более широкий тип?

Опять туплю.

Но типа доказать, что
Embed - это мономорфизм в категории аппликативов

Таки плохонько разобрался в коде.
Похоже на правду, но нет никакой уверенности, что это будет универсально.
Надо лучше разобраться, каким образом мы так кодируем Day~>Comp

У меня была мысль о том, что раз у нас всё сильное, то мы можем говорить просто о получении монады из моноидального функтора.

Раз вы тут развели хаскель, то подскажите по агде. Как мне в ней нормально "наследование" сделать? Например я доказал ряд свойств моноида, теперь хочу в группе их использовать. Я пока только такой путь вижу: описать их как разные дататайпы и задать "забывающее" преобразование из группы в моноид, а потом явно его использовать. Но это не очень удобно

Пытался на модулях что-нибудь придумать, но, как мне кажется, они больше на internal работу расчитаны. Не смог придумать как их заюзать

P.S. Похоже я нашёл что искал — https://agda.readthedocs.io/en/v2.5.2/language/record-types.html#instance-fields

Maybe you wanna know that "cofriend" will become a book in a few months

under CUP

same lecture note series of Kelly's book on enriched categories ❤

Fo Uche это автор https://arxiv.org/abs/1501.02503

То есть, он дополнит статью, предположительно, закруглив немного острые места?

Да, расжёвывания этой темы очень не хватает.

расширит и углубит!

страшно звучит

Constructing Applicative Functors
Ross Paterson
http://www.staff.city.ac.uk/~ross/papers
#paper

Милевского и так читают, но специально сделаю две ссылки.