let kCat = ../../../Category/Cat/semigroupal

let Set = ../../../Category/Set/rig

let base = ../../../Category/Monoidal/extractCategory kCat

let vObject = Type

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

let object = Type

let cat = ../../../Category/Rig/extractMultiplicative kCat vObject object Set

in  λ(m : kCat.arrow object object) →
    λ(monoidal : ../../../Functor/Monoidal/Type object v cat cat m) →
    λ(a : object) →
        { map =
            λ(b : object) →
            λ(c : object) →
            λ(f : Set.arrow { _1 = b, _2 = m c }) →
              ( ../pair
                  m
                  ( ../../../Functor/Monoidal/extractFunctor
                      object
                      v
                      cat
                      cat
                      m
                      monoidal
                  )
              ).map
                { _1 = a, _2 = b }
                { _1 = a, _2 = c }
                { _1 =
                    λ(x : a) →
                      monoidal.unit a (λ(_ : Set.multiplicative.unit) → x)
                , _2 = f
                }
        }
      : ../../../Functor/Endo/Star/Type
          vObject
          object
          v
          (base vObject object cat)
          m
          (λ(b : object) → Set.additive.product { _1 = a, _2 = b })