let kCat = ../Category/Cat/semigroupal

let vObject = Type

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

let base = ../Category/Monoidal/extractCategory kCat vObject

in  λ(cObject : Kind) →
    λ(c : ../Category/Monoidal/Kind kCat vObject cObject) →
    λ(semigroupoid : ../Semigroupoid/Type cObject v (base cObject c) c.arrow) →
      let Day = ./Type cObject v c

      in  λ(f : kCat.arrow cObject vObject) →
          λ(g : kCat.arrow cObject vObject) →
              { map =
                  λ(a : cObject) →
                  λ(b : cObject) →
                  λ(fn : c.arrow { _1 = a, _2 = b }) →
                  λ(day : Day { _1 = f, _2 = g } a) →
                    day
                      (Day { _1 = f, _2 = g } b)
                      ( λ(d : { _1 : cObject, _2 : cObject }) →
                        λ(fn2 : c.arrow { _1 = c.product d, _2 = a }) →
                        λ(e : v.product { _1 = f d._1, _2 = g d._2 }) →
                        λ(r0 : vObject) →
                        λ(day0 : ./convolution cObject v c f g b r0) →
                          day0
                            d
                            ( semigroupoid.product
                                { _1 = c.product d, _2 = b }
                                ( λ(r : Type) →
                                  λ ( arrowsOut
                                    : ∀(z : cObject) →
                                      c.arrow { _1 = z, _2 = b } →
                                      c.arrow { _1 = c.product d, _2 = z } →
                                        r
                                    ) →
                                    arrowsOut a fn fn2
                                )
                            )
                            e
                      )
              }
            : ../Functor/Type
                vObject
                cObject
                vObject
                (base vObject v)
                (base cObject c)
                (base vObject v)
                (Day { _1 = f, _2 = g })