∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {M N : CategoryTheory.Comonad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X)
  (f_δ :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) =
        CategoryTheory.CategoryStruct.comp (M.δ.app X)
          (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))),
  CategoryTheory.CategoryStruct.comp
      (let __NatTrans := f.inv;
      { toNatTrans := __NatTrans, app_ε := ⋯, app_δ := ⋯ })
      (let __NatTrans := f.hom;
      { toNatTrans := __NatTrans, app_ε := f_ε, app_δ := f_δ }) =
    CategoryTheory.CategoryStruct.id N