The thing about good abstractions is that they have a computation all of their own. It is kind of the inverse of Stalin’s supposed dictum, “quantity has a quality all of its own”.
This is what I like about the type theory/CS-informed approach to category theory: where we think carefully about the flow of information, the distinction between family and fibration, etc .
With the right abstraction, you can compute MORE than with the wrong model.