let cat = ../Category/Cat/semigroupal

let Category = ../Category/Kind cat

let vObject = Type

in  λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(c : Category vObject cObject) →
    λ(d : Category vObject dObject) →
        { constraint = c.constraint
        , arrow =
            λ(a : { _1 : cObject, _2 : cObject }) →
              ∀(f : cat.arrow cObject dObject) →
                d.arrow { _1 = f a._1, _2 = f a._2 }
        }
      : ../Category/Kind cat vObject cObject