let cat = ../Category/Cat/semigroupal

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) →
    λ(c : Category cObject) →
    λ(dObject : Kind) →
    λ(d : Category dObject) →
    λ(f : cat.arrow dObject cObject) →
    λ(fFunctor : ../Functor/Type vObject dObject cObject v d c f) →
    λ(g : cat.arrow cObject dObject) →
    λ(adjunction : ../Adjunction/Type cObject dObject v c d f g) →
        { unit = adjunction.counit
        , product =
            λ(a : cObject) →
              fFunctor.map (g a) (g (f (g a))) (adjunction.unit (g a))
        }
      : ../Comonad/Type
          cObject
          c
          (./Type cObject dObject cObject { _1 = f, _2 = g })