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

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../../Category/Kind kCat Type vObject) →
    λ(cat : ../../Category/Monoidal/Kind kCat vObject object) →
    λ(f : kCat.arrow object object) →
        { strengthen :
            ∀(a : object) →
            ∀(b : object) →
              cat.arrow
                { _1 = cat.product { _1 = a, _2 = f b }
                , _2 = f (cat.product { _1 = a, _2 = b })
                }
        }
      ⩓ ../Endo/Type
          vObject
          object
          v
          (../../Category/Monoidal/extractCategory kCat vObject object cat)
          f