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) →
    λ(category : ../../../Category/Type object v cat) →
    λ(f : kCat.arrow object object) →
    λ(g : kCat.arrow object object) →
    λ ( functor
      : ./Type
          vObject
          object
          (../../../Category/Monoidal/extractCategory kCat Type vObject v)
          cat
          f
          g
      ) →
    λ(a : object) →
      functor.map (f a) a (category.unit (f a))