let cat = ../Category/Cat/semigroupal

let vObject = Type

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

in  λ(cObject : Kind) →
      let dObject = Type

      in  λ(c : ../Category/Kind cat vObject cObject) →
          λ(cCategory : ../Category/Type cObject v c) →
            let dCategory = ../Category/Set/category/instance

            let d =
                  ../Category/Monoidal/Cartesian/extractCategory
                    cat
                    vObject
                    dObject
                    ../Category/Set/monoidal/cartesian

            in  λ(f : cat.arrow cObject dObject) →
                λ ( functor
                  : ./Type
                      vObject
                      cObject
                      dObject
                      (../Category/Monoidal/extractCategory cat Type vObject v)
                      c
                      d
                      f
                  ) →
                  { unit =
                      λ(a : cObject) →
                      λ(eq : ../Eq/Type (f a)) →
                        ../Eq/eqfn
                          (f a)
                          (f a)
                          eq
                          (functor.map a a (cCategory.unit a))
                          (dCategory.unit (f a))
                  , composition =
                      λ(a : cObject) →
                      λ(b : cObject) →
                      λ(e : cObject) →
                      λ(eq : ../Eq/Type (f e)) →
                      λ(fn : c.arrow { _1 = b, _2 = e }) →
                      λ(gn : c.arrow { _1 = a, _2 = b }) →
                        ../Eq/eqfn
                          (f a)
                          (f e)
                          eq
                          ( functor.map
                              a
                              e
                              ( cCategory.product
                                  { _1 = a, _2 = e }
                                  ( λ(r : Type) →
                                    λ ( arrowsOut
                                      : ∀(z : cObject) →
                                        c.arrow { _1 = z, _2 = e } →
                                        c.arrow { _1 = a, _2 = z } →
                                          r
                                      ) →
                                      arrowsOut b fn gn
                                  )
                              )
                          )
                          ( dCategory.product
                              { _1 = f a, _2 = f e }
                              ( λ(r : Type) →
                                λ ( arrowsOut
                                  : ∀(z : dObject) →
                                    d.arrow { _1 = z, _2 = f e } →
                                    d.arrow { _1 = f a, _2 = z } →
                                      r
                                  ) →
                                  arrowsOut
                                    (f b)
                                    (functor.map b e fn)
                                    (functor.map a b gn)
                              )
                          )
                  }