let cat = ../Category/Cat/semigroupal

let vObject = Type

in  λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(d : ../Category/Kind cat vObject dObject) →
      let object = cat.arrow cObject dObject

      in    ( λ(f : { _1 : object, _2 : object }) →
                ∀(a : cObject) → d.arrow { _1 = f._1 a, _2 = f._2 a }
            )
          : cat.arrow (cat.product object object) vObject