∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {I : C} [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)]
  [inst_4 : CategoryTheory.BraidedCategory C] {X : CategoryTheory.Over I} {A : C}
  (v : A ⟶ (CategoryTheory.Over.sections I).obj X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (β_ A I).hom
        (CategoryTheory.MonoidalClosed.uncurry
          (CategoryTheory.CategoryStruct.comp v
            (CategoryTheory.ChosenPullbacksAlong.fst ((CategoryTheory.ihom I).map X.hom)
              (CategoryTheory.curryRightUnitorHom I)))))
      X.hom =
    ((CategoryTheory.toOver I).obj A).hom