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

let vObject = Type

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

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

in  λ(cObject : Kind) →
    λ(c : Category cObject) →
    λ(dObject : Kind) →
    λ(d : Category dObject) →
    λ(dCategory : ../../Category/Type dObject v d) →
    λ(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 : dObject) →
        { map =
            λ(g : cObject) →
            λ(h : cObject) →
            λ(fn : c.arrow { _1 = g, _2 = h }) →
              bifunctor.map
                { _1 = g, _2 = a }
                { _1 = h, _2 = a }
                { _1 = fn, _2 = dCategory.unit a }
        }
      : ../Type
          vObject
          cObject
          eObject
          (../../Category/Monoidal/extractCategory cat Type vObject v)
          c
          e
          (λ(g : cObject) → f { _1 = g, _2 = a })