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.

For example, the formula defining the Cartesian product of two sets $A$ and $B$ in ZF when interpreted as above yields the notion of the product of two objects in an arbitrary category. Specifically, we have $$a\in A\wedge b\in B$$ $$\iff$$ $$\exists ! c\in A\times B\big(\pi_A(c)=a\wedge\pi_B(c)=b\big).$$

Defining

$$a\in_Y^\mathcal{C} X\iff a:Y\to X\in{\bf Hom}_\mathcal{C}$$

and using the notation $f(a)=f\circ a$ for global elements $a$ into the domain of $f$, if we replace all instances of $\in$ above with $\in_A^\mathcal{C}$ and interpret functions acting on elements as suggested, we get precisely the notion of the product of two objects in an arbitrary category (after universally quantifying over all global elementhood relations).