let cat = ../Category/Cat/semigroupal

let Category = ../Category/Kind cat

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