let cat = ../Category/Cat/semigroupal

let vObject = Type

let v =
      ../Category/Monoidal/Cartesian/extractMonoidal
        cat
        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 =
            ../Category/Monoidal/Cartesian/extractCategory
              cat
              vObject
              dObject
              ../Category/Set/monoidal/cartesian

      let Lan = ./Type cObject cpObject cp

      in  λ(f : cat.arrow cObject cpObject) →
          λ(g : cat.arrow cObject dObject) →
              { map =
                  λ(a : cpObject) →
                  λ(b : cpObject) →
                  λ(h : cp.arrow { _1 = a, _2 = b }) →
                  λ(lan : Lan f g a) →
                  λ(r : Type) →
                  λ ( k
                    : ∀(c : cObject) →
                      cp.arrow { _1 = f c, _2 = b } →
                        d.arrow { _1 = g c, _2 = r }
                    ) →
                    lan
                      r
                      ( λ(c : cObject) →
                        λ(x : cp.arrow { _1 = f c, _2 = a }) →
                          k
                            c
                            ( cpSemigroupoid.product
                                { _1 = f c, _2 = b }
                                ( λ(r : Type) →
                                  λ ( arrowsOut
                                    : ∀(z : cpObject) →
                                      cp.arrow { _1 = z, _2 = b } →
                                      cp.arrow { _1 = f c, _2 = z } →
                                        r
                                    ) →
                                    arrowsOut a h x
                                )
                            )
                      )
              }
            : ../Functor/Type
                vObject
                cpObject
                dObject
                (../Category/Monoidal/extractCategory cat Type vObject v)
                cp
                d
                (Lan f g)