let kCat = ../Category/Cat/semigroupal

let vObject = Type

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

let vBase = ../Category/Monoidal/extractCategory kCat Type vObject v

in  λ(object : Kind) →
    λ(cat : ../Category/Kind kCat vObject object) →
    λ(semigroupoid : ../Semigroupoid/Type object v cat cat.arrow) →
    λ(m : kCat.arrow object object) →
    λ(functor : ../Functor/Endo/Type vObject object vBase cat m) →
    λ(monad : ./Type object cat m) →
        { map =
            λ(a : object) →
            λ(b : object) →
            λ(f : cat.arrow { _1 = a, _2 = m b }) →
              semigroupoid.product
                { _1 = m a, _2 = m b }
                ( λ(r : Type) →
                  λ ( arrowsOut
                    : ∀(z : object) →
                      cat.arrow { _1 = z, _2 = m b } →
                      cat.arrow { _1 = m a, _2 = z } →
                        r
                    ) →
                    arrowsOut
                      (m (m b))
                      (monad.product b)
                      (functor.map a (m b) f)
                )
        }
      : ../Functor/Star/Type vObject object vBase cat m m