let kCat = ./Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(v : ./Monoidal/Kind kCat Type vObject) →
    λ(cat : ./Kind kCat vObject object) →
    λ(category : ./Type object v cat) →
      category.{ product, hom } : ../Semigroupoid/Type object v cat cat.arrow