{-|
This cheats a bit on the unit, since `dObject` is Type, we don’t need a functor
**Set** → 𝒟.
-}
let cat = ../../Category/Cat/semigroupal

let vObject = Type

let MonoidalCategory = ../Monoidal/Kind cat vObject

in  λ(cObject : Kind) →
      let dObject = Type

      in  λ(v : ../Kind cat Type vObject) →
          λ(c : MonoidalCategory cObject) →
          λ(d : MonoidalCategory dObject) →
            let base = ../Monoidal/extractCategory cat vObject

            in      { unit = λ(x : cObject) → c.arrow { _1 = c.unit, _2 = x }
                    , product = ../../Day/Type cObject d c
                    }
                  ∧ ./category
                      cObject
                      dObject
                      v
                      (base cObject c)
                      (base dObject d)
                : MonoidalCategory (cat.arrow cObject dObject)