{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {X : C} →
          [inst_3 : CategoryTheory.ComonObj X] →
            {motive : CategoryTheory.IsCommComonObj X → Sort u} →
              (t : CategoryTheory.IsCommComonObj X) →
                ((comul_comm :
                      CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (β_ X X).hom =
                        CategoryTheory.ComonObj.comul) →
                    motive ⋯) →
                  motive t