let kCat = ../Category/Cat/semigroupal

let vObject = Type

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

let object = Type

let cat =
      ../Category/Monoidal/Cartesian/extractCategory
        kCat
        vObject
        object
        ../Category/Set/monoidal/cartesian

in    { unit = λ(a : object) → λ(x : a) → x
      , counit = λ(a : object) → λ(x : a) → x
      , leftAdjunct = λ(a : object) → λ(b : object) → λ(f : a → b) → f
      , rightAdjunct = λ(a : object) → λ(b : object) → λ(f : a → b) → f
      }
    : ../Adjunction/Type object object v cat cat (./Type object) (./Type object)