let cat = ../Category/Cat/semigroupal

let Category = ../Category/Kind cat

let vObject = Type

in  λ(cObject : Kind) →
    λ(cpObject : Kind) →
    λ(cp : Category vObject cpObject) →
      let dObject = Type

      in  λ(p : cat.arrow cObject cpObject) →
              ( λ(f : cat.arrow cObject dObject) →
                λ(a : cpObject) →
                  ∀(b : cObject) → cp.arrow { _1 = a, _2 = p b } → f b
              )
            : cat.arrow (cat.arrow cObject dObject) (cat.arrow cpObject dObject)