let cat = ../Category/Cat/semigroupal

let monoidalBase = ../Category/Monoidal/Cartesian/extractMonoidal cat

let base = ../Category/Monoidal/extractCategory cat

let vObject = Type

let v = monoidalBase Type vObject ../Category/Set/monoidal/cartesian

in  λ(cObject : Kind) →
    λ(cpObject : Kind) →
    λ(cp : ../Category/Kind cat vObject cpObject) →
    λ(cpSemigroupoid : ../Semigroupoid/Type cpObject v cp cp.arrow) →
      let dObject = Type

      let d =
            base
              vObject
              dObject
              (monoidalBase vObject dObject ../Category/Set/monoidal/cartesian)

      let Ran = ./Type cObject cpObject cp

      in  λ(p : cat.arrow cObject cpObject) →
          λ(f : cat.arrow cObject dObject) →
              { map =
                  λ(a : cpObject) →
                  λ(b : cpObject) →
                  λ(fn : cp.arrow { _1 = a, _2 = b }) →
                  λ(ran : Ran p f a) →
                  λ(c : cObject) →
                  λ(k : cp.arrow { _1 = b, _2 = p c }) →
                    ran
                      c
                      ( cpSemigroupoid.product
                          { _1 = a, _2 = p c }
                          ( λ(r : Type) →
                            λ ( arrowsOut
                              : ∀(z : cpObject) →
                                cp.arrow { _1 = z, _2 = p c } →
                                cp.arrow { _1 = a, _2 = z } →
                                  r
                              ) →
                              arrowsOut b k fn
                          )
                      )
              }
            : ../Functor/Type
                vObject
                cpObject
                dObject
                (base Type vObject v)
                cp
                d
                (Ran p f)