let cat = ../Category/Cat/semigroupal

let Functor = ../Functor/Type

let Adjunction = ./Type

let Comonad = ../Comonad/Type

let Compose = ../Compose/Type

let vObject = Type

let v =
      ../Category/Monoidal/Cartesian/extractCategory
        cat
        Type
        vObject
        ../Category/Set/monoidal/cartesian

let Category = ../Category/Kind cat vObject

in  λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(c : Category cObject) →
    λ(d : Category dObject) →
    λ(f : cat.arrow dObject cObject) →
    λ(functor : Functor vObject dObject cObject v d c f) →
    λ(g : cat.arrow cObject dObject) →
    λ(adjunction : Adjunction cObject dObject v c d f g) →
        { unit = adjunction.counit
        , product =
            λ(a : cObject) →
              functor.map (g a) (g (f (g a))) (adjunction.unit (g a))
        }
      : Comonad cObject c (Compose cObject dObject cObject { _1 = f, _2 = g })