>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.

- - -

EDIT: In response to a (now deleted) answer by user Varkor, I wish to clarify that by ‘the internal language of categories’ I mean the interpretation of the language of ZF inside a category where membership is interpreted as global membership and functions acting on elements are interpreted as arrows out of an object postcomposed with global elements of that object. I’m working right now, but will post more details/examples later tonight.