{-|

**NB**: Since this is currently forced to be in **Set**, it’s quite possible
that some of the uses of 𝒞 and 𝒟 are wrong, since the type system can’t
distinguish them. So take them with a grain of salt if you’re editing this file.

-}
let cat = ../../Category/Cat/semigroupal

let MonoidalFunctor = ../../Functor/Monoidal/Type

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

let vObject = Type

in  λ(cObject : Kind) →
    λ(v : ../../Category/Kind cat Type vObject) →
    λ ( vCategory
      : ../../Category/Type
          vObject
          (base vObject Type ../../Category/Set/monoidal/cartesian)
          v
      ) →
    λ(c : ../../Category/Monoidal/Kind cat vObject cObject) →
      let Day/convolution = ../../Day/convolution

      let dObject = Type

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

      let eObject = Type

      let e = base vObject eObject ../../Category/Set/monoidal/cartesian

      let Compose = ../Type cObject dObject eObject

      let Day = ../../Day/Type cObject e c

      in  λ(f : cat.arrow dObject eObject) →
          λ(fMonoidal : MonoidalFunctor dObject v d e f) →
          λ(g : cat.arrow cObject dObject) →
          λ(gMonoidal : MonoidalFunctor cObject v c d g) →
              { map =
                  λ(a : cObject) →
                  λ(b : cObject) →
                    vCategory.product
                      { _1 = c.arrow { _1 = a, _2 = b }
                      , _2 = e.arrow { _1 = f (g a), _2 = f (g b) }
                      }
                      ( λ(r : Type) →
                        λ ( arrowsOut
                          : ∀(z : vObject) →
                            v.arrow
                              { _1 = z
                              , _2 = e.arrow { _1 = f (g a), _2 = f (g b) }
                              } →
                            v.arrow
                              { _1 = c.arrow { _1 = a, _2 = b }, _2 = z } →
                              r
                          ) →
                          arrowsOut
                            (d.arrow { _1 = g a, _2 = g b })
                            (fMonoidal.map (g a) (g b))
                            (gMonoidal.map a b)
                      )
              , unit =
                  λ(a : cObject) →
                  λ(fn : c.arrow { _1 = c.unit, _2 = a }) →
                    fMonoidal.unit (g a) (λ(_ : d.unit) → gMonoidal.unit a fn)
              , product =
                  λ(i : cObject) →
                  λ ( day
                    : Day
                        { _1 = Compose { _1 = f, _2 = g }
                        , _2 = Compose { _1 = f, _2 = g }
                        }
                        i
                    ) →
                    day
                      (f (g i))
                      ( λ(b : { _1 : cObject, _2 : cObject }) →
                        λ(fn : c.arrow { _1 = c.product b, _2 = i }) →
                        λ(a : { _1 : f (g b._1), _2 : f (g b._2) }) →
                          fMonoidal.product
                            (g i)
                            ( λ(fr : eObject) →
                              λ ( fDay
                                : Day/convolution dObject e d f f (g i) fr
                                ) →
                                fDay
                                  { _1 = g b._1, _2 = g b._2 }
                                  ( λ(p : { _1 : g b._1, _2 : g b._2 }) →
                                      gMonoidal.product
                                        i
                                        ( λ(gr : dObject) →
                                          λ ( gDay
                                            : Day/convolution
                                                cObject
                                                d
                                                c
                                                g
                                                g
                                                i
                                                gr
                                            ) →
                                            gDay b fn p
                                        )
                                  )
                                  a
                            )
                      )
              }
            : MonoidalFunctor cObject v c e (Compose { _1 = f, _2 = g })