let cat = ../Category/Cat/semigroupal

let Functor = ../Functor/Type

let Adjunction = ./Type

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