Is there a procedure we can use to work in the internal language of a $2$-category and thereby avoid pasting diagram chases, in the same way that the internal language of a category can help us avoid diagram chases?
I ask because the one dimensional version of this procedure makes very good sense to me, and frequently makes proofs as intuitively easy as they feel like they ‘should be’ as opposed to big pictorial things (not that pictures aren’t nice sometimes). Any pointers are appreciated.