let cat = ../Category/Cat/semigroupal

let vObject = Type

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

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

in  λ(cObject : Kind) →
    λ(cpObject : Kind) →
    λ(dObject : Kind) →
    λ(cp : Category/Kind cpObject) →
    λ(d : Category/Kind dObject) →
    λ(dSemigroupoid : ../Semigroupoid/Type dObject v d d.arrow) →
    λ(h : cat.arrow cpObject dObject) →
    λ ( functor
      : ../Functor/Type
          vObject
          cpObject
          dObject
          (../Category/Monoidal/extractCategory cat Type vObject v)
          cp
          d
          h
      ) →
    λ(f : cat.arrow cObject cpObject) →
    λ(g : cat.arrow cObject dObject) →
    λ(join : ∀(b : cObject) → d.arrow { _1 = h (f b), _2 = g b }) →
    λ(a : cpObject) →
    λ(b : cObject) →
    λ(k : cp.arrow { _1 = a, _2 = f b }) →
      dSemigroupoid.product
        { _1 = h a, _2 = g b }
        ( λ(r : Type) →
          λ ( arrowsOut
            : ∀(z : dObject) →
              d.arrow { _1 = z, _2 = g b } →
              d.arrow { _1 = h a, _2 = z } →
                r
            ) →
            arrowsOut (h (f b)) (join b) (functor.map a (f b) k)
        )