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) →
                  ∀(r : Type) →
                  (∀(b : cObject) → cp.arrow { _1 = p b, _2 = a } → f b → r) →
                    r
              )
            : cat.arrow (cat.arrow cObject dObject) (cat.arrow cpObject dObject)