let cat = ../Category/Cat/semigroupal

in  λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(eObject : Kind) →
        ( λ ( f
            : { _1 : cat.arrow dObject eObject, _2 : cat.arrow cObject dObject }
            ) →
          λ(a : cObject) →
            f._1 (f._2 a)
        )
      : cat.arrow
          (cat.product (cat.arrow dObject eObject) (cat.arrow cObject dObject))
          (cat.arrow cObject eObject)