let kCat = ../Category/Cat/semigroupal

let vObject = Type

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

in  λ(object : Kind) →
    λ(cat : ../Category/Kind kCat vObject object) →
    λ(semigroupoid : ../Semigroupoid/Type object v cat cat.arrow) →
    λ(f : kCat.arrow object object) →
    λ ( functor
      : ../Functor/Endo/Type
          vObject
          object
          (../Category/Monoidal/extractCategory kCat Type vObject v)
          cat
          f
      ) →
    λ(monad : ../Monad/Type object cat f) →
      ../Ran/lift
        object
        object
        object
        cat
        cat
        semigroupoid
        f
        functor
        f
        f
        monad.product