∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G : C)
  {X Y : C} (g : X ⟶ Y) (X_1 : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C).obj G).map g).app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X_1 G).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X_1)
          G)
        (CategoryTheory.MonoidalCategoryStruct.associator Y X_1 G).hom)