let cat = ../Category/Cat/semigroupal

let MonoidalCategory = ../Category/Monoidal/Kind cat

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

let vObject = Type

in  λ(cObject : Kind) →
    λ(v : MonoidalCategory Type vObject) →
    λ(c : MonoidalCategory vObject cObject) →
        ( λ ( f
            : { _1 : cat.arrow cObject vObject, _2 : cat.arrow cObject vObject }
            ) →
            ../Lan/Type
              { _1 : cObject, _2 : cObject }
              cObject
              (base vObject cObject c)
              c.product
              ( λ(p : { _1 : cObject, _2 : cObject }) →
                  v.product { _1 = f._1 p._1, _2 = f._2 p._2 }
              )
        )
      : cat.arrow
          (cat.product (cat.arrow cObject vObject) (cat.arrow cObject vObject))
          (cat.arrow cObject vObject)