no goals
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ map f g ≫ (braiding Y W).hom = (braiding X Z).hom ≫ map g f
aesop_cat