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