let cat = ../Category/Cat/semigroupal

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

let vObject = Type

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

in  λ(cObject : Kind) →
    λ(cpObject : Kind) →
    λ(cp : ../Category/Kind cat vObject cpObject) →
      let dSemigroupoid = ../Category/Set/semigroupoid

      let dObject = Type

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

      in  λ(h : cat.arrow cpObject dObject) →
          λ(functor : ../Functor/Type vObject cpObject dObject v cp d h) →
          λ(f : cat.arrow cObject cpObject) →
          λ(g : cat.arrow cObject dObject) →
          λ(duplicate : ∀(b : cObject) → d.arrow { _1 = g b, _2 = h (f b) }) →
          λ(a : cpObject) →
          λ(lan : ./Type cObject cpObject cp f g a) →
            lan
              (h a)
              ( λ(b : cObject) →
                λ(k : cp.arrow { _1 = f b, _2 = a }) →
                  dSemigroupoid.product
                    { _1 = g b, _2 = h a }
                    ( λ(r : Type) →
                      λ ( arrowsOut
                        : ∀(z : dObject) →
                          d.arrow { _1 = z, _2 = h a } →
                          d.arrow { _1 = g b, _2 = z } →
                            r
                        ) →
                        arrowsOut
                          (h (f b))
                          (functor.map (f b) a k)
                          (duplicate b)
                    )
              )