{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (obj : C → C) →
      (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) →
        (map_id :
            autoParam (∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
              CategoryTheory.Functor.map_id._autoParam) →
          (map_comp :
              autoParam
                (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
                  map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g))
                CategoryTheory.Functor.map_comp._autoParam) →
            (ε : { obj := obj, map := map, map_id := map_id, map_comp := map_comp } ⟶ CategoryTheory.Functor.id C) →
              (δ :
                  { obj := obj, map := map, map_id := map_id, map_comp := map_comp } ⟶
                    { obj := obj, map := map, map_id := map_id, map_comp := map_comp }.comp
                      { obj := obj, map := map, map_id := map_id, map_comp := map_comp }) →
                autoParam
                    (∀ (X : C),
                      CategoryTheory.CategoryStruct.comp (δ.app X) (map (δ.app X)) =
                        CategoryTheory.CategoryStruct.comp (δ.app X) (δ.app (obj X)))
                    CategoryTheory.Comonad.coassoc._autoParam →
                  autoParam
                      (∀ (X : C),
                        CategoryTheory.CategoryStruct.comp (δ.app X) (ε.app (obj X)) =
                          CategoryTheory.CategoryStruct.id (obj X))
                      CategoryTheory.Comonad.left_counit._autoParam →
                    autoParam
                        (∀ (X : C),
                          CategoryTheory.CategoryStruct.comp (δ.app X) (map (ε.app X)) =
                            CategoryTheory.CategoryStruct.id (obj X))
                        CategoryTheory.Comonad.right_counit._autoParam →
                      CategoryTheory.Comonad C