∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  {X x : CategoryTheory.Cokleisli U} (f : X ⟶ x),
  (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).map f = CategoryTheory.CategoryStruct.comp (U.δ.app X) (U.map f)