let kCat = ./Cat/semigroupal

let vObject = Type

let v =
      ./Monoidal/Cartesian/extractMonoidal
        kCat
        Type
        vObject
        ./Set/monoidal/cartesian

let vBase = ./Monoidal/extractCategory kCat Type vObject v

in  λ(object : Kind) →
    λ(cat : ./Kind kCat vObject object) →
    λ(category : ./Type object v cat) →
    λ(c : object) →
        { map =
            λ(x : object) →
            λ(y : object) →
            λ(fn : cat.arrow { _1 = y, _2 = x }) →
            λ(input : cat.arrow { _1 = x, _2 = c }) →
              category.product
                { _1 = y, _2 = c }
                ( λ(r : Type) →
                  λ ( arrowsOut
                    : ∀(z : object) →
                      cat.arrow { _1 = z, _2 = c } →
                      cat.arrow { _1 = y, _2 = z } →
                        r
                    ) →
                    arrowsOut x input fn
                )
        }
      : ../Functor/Contravariant
          vObject
          object
          vObject
          vBase
          cat
          vBase
          (λ(x : object) → cat.arrow { _1 = x, _2 = c })