{-|
A profunctor `𝒞 ↛ 𝒟` is represented as the bifunctor `(𝒟^op, 𝒞) → 𝒱`. This is
much more general than Haskell’s `Profunctor`. It also requires that 𝒱 is
closed.
-}
let cat = ../../Category/Cat/semigroupal

let Category = ../../Category/Kind cat

let vObject = Type

in  λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(v : ../../Category/Monoidal/Closed/Kind cat vObject) →
    λ(c : Category vObject cObject) →
    λ(d : Category vObject dObject) →
      ../Bifunctor/Type
        vObject
        dObject
        cObject
        vObject
        v
        (../../Category/Op/Kind vObject dObject d)
        c
        (../../Category/Monoidal/extractCategory cat vObject vObject v)