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 : W ⟶ Y
g : X ⟶ Z
⊢ (braiding X W).hom ≫ map f g ≫ (braiding Y Z).hom = map g f
aesop_cat