{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {X : C} →
          {motive : CategoryTheory.HopfObj X → Sort u} →
            (t : CategoryTheory.HopfObj X) →
              ([toBimonObj : CategoryTheory.BimonObj X] →
                  (antipode : X ⟶ X) →
                    (antipode_left :
                        CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight antipode X)
                              CategoryTheory.MonObj.mul) =
                          CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one) →
                      (antipode_right :
                          CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X antipode)
                                CategoryTheory.MonObj.mul) =
                            CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit
                              CategoryTheory.MonObj.one) →
                        motive
                          { toBimonObj := toBimonObj, antipode := antipode, antipode_left := antipode_left,
                            antipode_right := antipode_right }) →
                motive t