A formal system of category theory is no more abstract than a formal system of natural numbers. The apparent difference in abstraction is relative to the subjective (and irrelevant) choice of application. Category theory seems abstract for counting jelly beans, but for other applications it might be less of an abstraction than arithmetic.
https://math.stackexchange.com/questions/298912/real-world-a...
Similar to how computer programs can be broken down into physical laws about the movement of electrons, mathematical proofs can be broken down into deductive statements about ZFC set theory, etc. In both cases this is ideally about concretely building upon previous work, not creating abstractions.
The problem of incomprehensible proofs isn't about a "tower of abstraction". There's no abstraction within formal systems. The system is described and the implications are deduced. The problem is expanding complexity with a lack of detail and exposition that allows for misunderstandings and perhaps even errors.