let cat = ../Cat/semigroupal

let vObject = Type

let Category = ../Kind cat vObject

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

      in    { constraint =
                λ(x : object) →
                  { _1 : c.constraint x._1, _2 : d.constraint x._2 }
            , arrow =
                λ(a : cat.product object object) →
                  v.product
                    { _1 = c.arrow { _1 = a._1._1, _2 = a._2._1 }
                    , _2 = d.arrow { _1 = a._1._2, _2 = a._2._2 }
                    }
            }
          : Category object