let cat = ../../Category/Cat/semigroupal

let vObject = Type

let v =
      ../../Category/Monoidal/Cartesian/extractMonoidal
        cat
        Type
        vObject
        ../../Category/Set/monoidal/cartesian

let Category = ../../Category/Kind cat vObject

in  λ(cObject : Kind) →
    λ(c : Category cObject) →
    λ(cCategory : ../../Category/Type cObject v c) →
    λ(dObject : Kind) →
    λ(d : Category dObject) →
    λ(eObject : Kind) →
    λ(e : Category eObject) →
    λ(f : cat.arrow (cat.product cObject dObject) eObject) →
    λ(bifunctor : ./Type vObject cObject dObject eObject v c d e f) →
    λ(a : cObject) →
        { map =
            λ(b : dObject) →
            λ(c : dObject) →
            λ(fn : d.arrow { _1 = b, _2 = c }) →
              bifunctor.map
                { _1 = a, _2 = b }
                { _1 = a, _2 = c }
                { _1 = cCategory.unit a, _2 = fn }
        }
      : ../Type
          vObject
          dObject
          eObject
          (../../Category/Monoidal/extractCategory cat Type vObject v)
          d
          e
          (λ(b : dObject) → f { _1 = a, _2 = b })