∀ (B : Type u_1) [inst : CategoryTheory.Bicategory B] (C : Type u_2) [inst_1 : CategoryTheory.Bicategory C]
  {a b c d : B × C} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).hom.1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f.1 g.1 h.1).hom
        (CategoryTheory.eqToHom ⋯))