Thanks for this informative comment! By all means, it would be great to hear more about it.

Here you're making the argument that things are not so simple with Haskell.

I still wonder though to what extent it is true within pure category theory. At least for the basic stuff I've going through, almost all the weight of the matter has been concentrated in the definitions rather than the proofs. Does this trend continue into the more advanced realms of category theory?