let cat = ../Category/Cat/semigroupal

let Category = ../Category/Kind cat

let vObject = Type

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

in  λ(cObject : Kind) →
    λ(c : Category vObject cObject) →
    λ(dObject : Kind) →
    λ(d : Category vObject dObject) →
    λ(dCategory : ../Category/Type dObject v d) →
      let object = cat.arrow cObject dObject

      let arrow = ./Type cObject dObject d

      let compose =
            λ(a : { _1 : object, _2 : object }) →
            λ ( p
              : ∀(r : Type) →
                ( ∀(z : object) →
                  arrow { _1 = z, _2 = a._2 } →
                  arrow { _1 = a._1, _2 = z } →
                    r
                ) →
                  r
              ) →
            λ(i : cObject) →
              dCategory.product
                { _1 = a._1 i, _2 = a._2 i }
                ( λ(r : Type) →
                  λ ( arrowsOut
                    : ∀(z : dObject) →
                      d.arrow { _1 = z, _2 = a._2 i } →
                      d.arrow { _1 = a._1 i, _2 = z } →
                        r
                    ) →
                    p
                      r
                      ( λ(z : object) →
                        λ(f : arrow { _1 = z, _2 = a._2 }) →
                        λ(g : arrow { _1 = a._1, _2 = z }) →
                          arrowsOut (z i) (f i) (g i)
                      )
                )

      in    { unit = λ(a : object) → λ(i : cObject) → dCategory.unit (a i)
            , product = compose
            , hom.map
              =
                λ(a : cat.product object object) →
                λ(b : cat.product object object) →
                λ ( f
                  : v.product
                      { _1 = arrow { _1 = b._1, _2 = a._1 }
                      , _2 = arrow { _1 = a._2, _2 = b._2 }
                      }
                  ) →
                λ(fn : arrow a) →
                  compose
                    { _1 = b._1, _2 = b._2 }
                    ( λ(r : Type) →
                      λ ( arrowsOut
                        : ∀(z : object) →
                          arrow { _1 = z, _2 = b._2 } →
                          arrow { _1 = b._1, _2 = z } →
                            r
                        ) →
                        arrowsOut
                          a._1
                          ( compose
                              { _1 = a._1, _2 = b._2 }
                              ( λ(r : Type) →
                                λ ( arrowsOut
                                  : ∀(z : object) →
                                    arrow { _1 = z, _2 = b._2 } →
                                    arrow { _1 = a._1, _2 = z } →
                                      r
                                  ) →
                                  arrowsOut a._2 f._2 fn
                              )
                          )
                          f._1
                    )
            }
          : ../Category/Type
              object
              v
              ( ../Category/Functor/category
                  cObject
                  dObject
                  (../Category/Monoidal/extractCategory cat Type vObject v)
                  c
                  d
              )