∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {X Y : B × C}
  (a : X ⟶ Y), (CategoryTheory.Bicategory.Prod.swap B C).map a = CategoryTheory.Prod.mkHom a.2 a.1