{-|

This doesn’t use `extractSemigroupal` because I don’t know how to apply the
`morphism` in the monoidal category instance.
-}
let kCat = ../../Category/Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../../Category/Monoidal/Kind kCat Type vObject) →
    λ(cat : ../Kind kCat vObject object) →
      let profunctor = kCat.arrow (kCat.product object object) vObject

      in    { constraint = ../../Functor/Profunctor/Type object object v cat cat
            , arrow =
                λ(p : { _1 : profunctor, _2 : profunctor }) →
                  ∀(a : { _1 : object, _2 : object }) → p._1 a → p._2 a
            , product =
                λ(p : { _1 : profunctor, _2 : profunctor }) →
                λ(a : { _1 : object, _2 : object }) →
                  ∀(r : Type) →
                  ( ∀(z : object) →
                    p._1 { _1 = z, _2 = a._2 } →
                    p._2 { _1 = a._1, _2 = z } →
                      r
                  ) →
                    r
            }
          : ../Semigroupal/Kind kCat vObject profunctor