let cat = ../Category/Cat/semigroupal

in  λ(vObject : Kind) →
    λ(cObject : Kind) →
    λ(dObject : Kind) →
    λ(v : ../Category/Kind cat Type vObject) →
    λ(c : ../Category/Kind cat vObject cObject) →
    λ(d : ../Category/Kind cat vObject dObject) →
    λ(f : cat.arrow cObject dObject) →
    λ(functor : ./Type vObject cObject dObject v c d f) →
        { map = λ(a : cObject) → λ(b : cObject) → functor.map b a }
      : ./Type
          vObject
          cObject
          dObject
          v
          (../Category/Op/Kind vObject cObject c)
          (../Category/Op/Kind vObject dObject d)
          f