let cat = ../Category/Cat/semigroupal

let vObject = Type

let MonoidalCategory = ../Category/Monoidal/Kind cat

in  λ(cObject : Kind) →
    λ(v : MonoidalCategory Type vObject) →
    λ(c : MonoidalCategory vObject cObject) →
    λ(f : cat.arrow cObject vObject) →
    λ(g : cat.arrow cObject vObject) →
    λ(a : cObject) →
    λ(r : vObject) →
      ∀(b : { _1 : cObject, _2 : cObject }) →
      c.arrow { _1 = c.product b, _2 = a } →
        v.arrow { _1 = v.product { _1 = f b._1, _2 = g b._2 }, _2 = r }