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

let Functor = ../../Functor/Type

let Category = ../../Category/Kind cat

in  λ(vObject : Kind) →
    λ(v : Category Type vObject) →
    λ ( vCategory
      : ../../Category/Type
          vObject
          ( ../../Category/Monoidal/Cartesian/extractMonoidal
              cat
              Type
              Type
              ../../Category/Set/monoidal/cartesian
          )
          v
      ) →
    λ(cObject : Kind) →
    λ(c : Category vObject cObject) →
    λ(dObject : Kind) →
    λ(d : Category vObject dObject) →
    λ(eObject : Kind) →
    λ(e : Category vObject eObject) →
    λ(f : cat.arrow dObject eObject) →
    λ(fFunctor : Functor vObject dObject eObject v d e f) →
    λ(g : cat.arrow cObject dObject) →
    λ(gFunctor : Functor vObject cObject dObject 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 })
                      (fFunctor.map (g a) (g b))
                      (gFunctor.map a b)
                )
        }
      : Functor
          vObject
          cObject
          eObject
          v
          c
          e
          (../Type cObject dObject eObject { _1 = f, _2 = g })