let cat = ../Category/Cat/semigroupal

let monoidalBase = ../Category/Monoidal/Cartesian/extractMonoidal cat

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

let vObject = Type

let v =
      base
        Type
        vObject
        (monoidalBase Type vObject ../Category/Set/monoidal/cartesian)

let cObject = Type

let cpObject = Type

let dObject = Type

let c = monoidalBase vObject cObject ../Category/Set/monoidal/cartesian

let cp = monoidalBase vObject cpObject ../Category/Set/monoidal/cartesian

in  λ(p : cat.arrow cObject cpObject) →
    λ(monoidal : ../Functor/Monoidal/Type cObject v c cp p) →
    λ(f : cat.arrow cObject dObject) →
    λ(a : cpObject) →
    λ(ran : ./Type cObject cpObject (base vObject cpObject cp) p f a) →
      ran a (λ(x : a) → monoidal.unit a (λ(_ : c.unit) → x))