∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : C}
  (h : T.obj (T.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T.map f) (CategoryTheory.CategoryStruct.comp (T.δ.app Y) h) =
    CategoryTheory.CategoryStruct.comp (T.δ.app X) (CategoryTheory.CategoryStruct.comp (T.map (T.map f)) h)