# modularizing category theory

I have made the experience that proofs using category theory often look very elegant and short but when it comes down to verifying the details there is quite a list of commutativities etc. to check. A typical example is verifying that some functor preserves some limits: often only the tips of the cones are considered and it remains for the reader to check how the argument extends to the rest of the cones. On the other hand checking these details is usually very straightforward and “canonical”, $-$ all goes as one expects.

This got me wondering whether it wouldn't be possible to modularize category theory more, so as to avoid repeating the same arguments over and over again in similar situations. I am sure higher category theory could be a very good tool for achieving this and maybe it has already been done, so I thought I might ask here whether someone could recommend books. I would also be interested to hear what others think about this “problem” or whether they even consider it as such.

I know that I am not being very concrete here but I am hoping that those of you who have made the same experience will know what I mean.

• Only some comments: (0) Your "question" does not contain any question mark. (1) this MO thread is somewhat in the spirit of your question. – Peter Heinig Jul 15 '17 at 16:08