∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.ε.app (self.obj X)) =
    CategoryTheory.CategoryStruct.id (self.obj X)