There's maybe a two-to-three-order-of-magnitude difference between the difficulty of monads and the difficulty of this stuff.
but is the relative difficulty, in human understanding, or a 'fundamental' difference in complexity?
surely the later is something mathematicians can and have measured?
You could try to draw the stack of abstractions necessary to understand the proof and see how high it stacks, and you could try to call that fundamental complexity, but I don't think many people would be happy with that.
So yes, it's a difficulty in human understanding. What else could it be?