Working in a set theoretical background, when we express various categorical coherence conditions by expanding all definitions involved back down to a set-theoretical level, what we end up with are statements with multiple universal quantifiers outside of them. For example, consider the following $2$-d diagram:

To express that this diagram commutes at the set theoretical level, we would write

$$\forall\Sigma\in{\bf Ob}_{\mathbb{S}ig}\forall M\in{\bf Ob}_{{\sf Mod}(\Sigma)}\forall e'\in{\sf Sen}'(\Phi(\Sigma))\Big(M\models_\Sigma\alpha_\Sigma(e')\iff\beta_\Sigma(M)\models_{\Phi(\Sigma)}e'\Big).$$

But to express that this diagram commutes at the $2$-d categorical level, we just say the diagram commutes or write $$(\models'\star1_{\Phi^{op}})\circ\beta=\alpha^\dagger\circ\models.$$

This statement contains exactly the same information as the one above it, but without any quantification by virtue of wrapping all the pieces together and expressing their interplay 'at a higher level'.

Is this process a version of quantifier elimination? More generally, what does quantifier elimination look like from the perspective of higher category theory?

We can get 'there exists' quantifiers mixed in with the 'for all's if we choose the correct codomain category, and these also vanish when we express things higher dimensionally. Any pointers are appreciated, and if this question is trivial from a logical perspective I apologize in advance :^).

Working in a set theoretical background, when we express various categorical coherence conditions by expanding all definitions involved back down to a set-theoretical level, what we end up with are statements with multiple universal quantifiers outside of them. For example, consider the following $2$-d diagram:

To express that this diagram commutes at the set theoretical level, we would write

$$\forall\Sigma\in{\bf Ob}_{\mathbb{S}ig}\forall M\in{\bf Ob}_{{\sf Mod}(\Sigma)}\forall e'\in{\sf Sen}'(\Phi(\Sigma))\Big(M\models_\Sigma\alpha_\Sigma(e')\iff\beta_\Sigma(M)\models'_{\Phi(\Sigma)}e'\Big).$$

But to express that this diagram commutes at the $2$-d categorical level, we just say the diagram commutes or write $$(\models'\star1_{\Phi^{op}})\circ\beta=\alpha^\dagger\circ\models.$$

This statement contains exactly the same information as the one above it, but without any quantification by virtue of wrapping all the pieces together and expressing their interplay 'at a higher level'.

Is this process a version of quantifier elimination? More generally, what does quantifier elimination look like from the perspective of higher category theory?

We can get 'there exists' quantifiers mixed in with the 'for all's if we choose the correct codomain category, and these also vanish when we express things higher dimensionally. Any pointers are appreciated, and if this question is trivial from a logical perspective I apologize in advance :^).