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

let vObject = Type

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

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