let cat = ../Category/Cat/semigroupal

let vObject = Type

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

let base = ../Category/Monoidal/extractCategory cat Type vObject v

in  λ(semigroupoid : ../Semigroupoid/Type vObject v base v.arrow) →
      let Comonad = ../Comonad/Type vObject base

      let Day = ./Type vObject v v

      let Day/convolution = ../Day/convolution vObject v v

      in  λ(f : cat.arrow vObject vObject) →
          λ(fComonad : Comonad f) →
          λ(g : cat.arrow vObject vObject) →
          λ(gComonad : Comonad g) →
              { unit =
                  λ(a : vObject) →
                  λ(day : Day { _1 = f, _2 = g } a) →
                    day
                      a
                      ( λ(b : { _1 : vObject, _2 : vObject }) →
                        λ(fn : { _1 : b._1, _2 : b._2 } → a) →
                        λ(d : { _1 : f b._1, _2 : g b._2 }) →
                          fn
                            { _1 = fComonad.unit b._1 d._1
                            , _2 = gComonad.unit b._2 d._2
                            }
                      )
              , product =
                  λ(a : vObject) →
                  λ(day : Day { _1 = f, _2 = g } a) →
                    day
                      (Day { _1 = f, _2 = g } (Day { _1 = f, _2 = g } a))
                      ( λ(b : { _1 : vObject, _2 : vObject }) →
                        λ(fn : { _1 : b._1, _2 : b._2 } → a) →
                        λ(d : { _1 : f b._1, _2 : g b._2 }) →
                        λ(r0 : vObject) →
                        λ ( day0
                          : Day/convolution f g (Day { _1 = f, _2 = g } a) r0
                          ) →
                          day0
                            { _1 = f b._1, _2 = g b._2 }
                            ( λ(p : { _1 : f b._1, _2 : g b._2 }) →
                              λ(r1 : vObject) →
                              λ(day1 : Day/convolution f g a r1) →
                                day1 b fn p
                            )
                            { _1 = fComonad.product b._1 d._1
                            , _2 = gComonad.product b._2 d._2
                            }
                      )
              }
            : Comonad (Day { _1 = f, _2 = g })