{-|
A contravariant functor `C → D` is equivalent to a covariant functor `C^op → D`.
-}
let cat = ../Category/Cat/semigroupal

in  λ(vObject : Kind) →
    λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(v : ../Category/Kind cat Type vObject) →
    λ(c : ../Category/Kind cat vObject cObject) →
      ./Type vObject cObject dObject v (../Category/Op/Kind vObject cObject c)