{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Comon C} →
        {motive : M.Hom N → Sort u} →
          ((hom : M.X ⟶ N.X) →
              [isComonHom_hom : CategoryTheory.IsComonHom hom] →
                motive { hom := hom, isComonHom_hom := isComonHom_hom }) →
            (t : M.Hom N) → motive t