let cat = ../Category/Cat/semigroupal

let Category = ../Category/Kind cat

let vObject = Type

in  λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(v : Category Type vObject) →
    λ(c : Category vObject cObject) →
    λ(d : Category vObject dObject) →
    λ(f : cat.arrow dObject cObject) →
    λ(g : cat.arrow cObject dObject) →
      { unit : ∀(a : dObject) → d.arrow { _1 = a, _2 = g (f a) }
      , counit : ∀(a : cObject) → c.arrow { _1 = f (g a), _2 = a }
      , leftAdjunct :
          ∀(a : dObject) →
          ∀(b : cObject) →
            v.arrow
              { _1 = c.arrow { _1 = f a, _2 = b }
              , _2 = d.arrow { _1 = a, _2 = g b }
              }
      , rightAdjunct :
          ∀(a : dObject) →
          ∀(b : cObject) →
            v.arrow
              { _1 = d.arrow { _1 = a, _2 = g b }
              , _2 = c.arrow { _1 = f a, _2 = b }
              }
      }