let cat = ../Category/Cat/semigroupal

let Set = ../Category/Set/monoidal/cartesian

let base = ../Category/Monoidal/Cartesian/extractCategory cat

let vObject = Type

let v = base Type vObject ../Category/Set/monoidal/cartesian

in  λ(s : Type) →
        { unit = λ(a : Type) → λ(x : a) → λ(y : s) → { _1 = y, _2 = x }
        , counit = λ(a : Type) → λ(x : { _1 : s, _2 : s → a }) → x._2 x._1
        , leftAdjunct =
            λ(a : Type) →
            λ(b : Type) →
            λ(f : { _1 : s, _2 : a } → b) →
            λ(x : a) →
            λ(y : s) →
              f { _1 = y, _2 = x }
        , rightAdjunct =
            λ(a : Type) →
            λ(b : Type) →
            λ(f : a → s → b) →
            λ(t : { _1 : s, _2 : a }) →
              f t._2 t._1
        }
      : ../Adjunction/Type
          Type
          Type
          v
          (base vObject Type Set)
          (base vObject Type Set)
          (λ(a : Type) → Set.product { _1 = s, _2 = a })
          (λ(a : Type) → Set.arrow { _1 = s, _2 = a })