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

а щито не так?

Я что-то подозреваю.

Про partial monad'ы —
https://golem.ph.utexas.edu/category/2019/09/partial_evaluations_2.html
#paper

Йоу, налетайте! ;-)
In fact, an adjunction just extends a universal construction over the whole category (or two categories, in general).
It combines the mapping-in with the mapping-out conditions.
One functor (traditionally called the left adjoint) prepares the input for mapping out, and the other (the right adjoint) prepares the output for mapping in.
The trick is to find a pair of functors that complement each other:
there are as many mapping-outs from one functor as there are mappinins to the other functor.
https://bartoszmilewski.com/2019/09/20/the-power-of-adjunctions/
#paper

Ребят, а можно ли как-то простым образом доказать, что любая функция foo :: a -> a является id?

Это не в любой категории верно ;-)

Ну меня интересует Hask

А как это на языке теории категорий сформулировать вообще?

Hask не категория, да в нём это и не верно

эмм, а можно контрпример?

const undefined

я вот другой реализации не могу придумать

Хотя тут не особо доказывают.

Вадлер доказывает (Но не для Hask, естественно)

Если совсем строго, то надо описывать SystemF или хотябы часть её с квантификацией по типам.
А если этого не делать, то получаются очевидно неверные вещи, типа что любая стрелка, у которой домен совпадает с кодоменом, является id-стрелкой.