{-|
A presheaf on a category 𝒞 is a functor 𝒞 ^op^ → 𝐒𝐞𝐭.
-}
let cat = ../Category/Cat/semigroupal

let Category = ../Category/Kind cat

let vObject = Type

in  λ(cObject : Kind) →
    λ(v : Category Type vObject) →
    λ(c : Category vObject cObject) →
      ../Functor/Type
        vObject
        cObject
        Type
        v
        (../Category/Op/Kind vObject cObject c)
        ( ../Category/Monoidal/Cartesian/extractCategory
            cat
            vObject
            Type
            ../Category/Set/monoidal/cartesian
        )