I believe they are higher dimensional string diagrams. Maybe called n-diagrams? They are used in higher homotopy and higher category theory, I believe. But not entirely sure.

https://arxiv.org/pdf/2305.06938

EDIT: Found it! they are called surface diagram, which are generalization of string diagram to 3-categories https://golem.ph.utexas.edu/category/2010/03/modeling_surface_diagrams.html https://ncatlab.org/nlab/show/surface+diagram

Still not sure what the proof is talking about though :(

But from the conclusion it looks like some sort of natruality condition, where the morphisms are slided around except beta.

EDIT AGAIN: got in touch with my string diagram contact. Here is the paper https://arxiv.org/pdf/0807.0658

Note the conclusion at the bottom, the proof on the right and the axiom on the left doesn't seem to be related.

The proof on the right is Theorem 6; the equality at bottom is in section 3.4, where the proof is omitted because "follows from definition"; the axiom on the left is HM1 and HM2 on page 19.