let kCat = ../Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../Monoidal/Kind kCat Type vObject) →
    λ(cat : ./Kind kCat vObject object) →
      let base = ./extractCategory kCat vObject object cat

      let Isomorphism = ../../Isomorphism/Type object base

      in    { associativity :
                ∀(a : object) →
                ∀(b : object) →
                ∀(c : object) →
                  Isomorphism
                    { _1 =
                        cat.product
                          { _1 = cat.product { _1 = a, _2 = b }, _2 = c }
                    , _2 =
                        cat.product
                          { _1 = a, _2 = cat.product { _1 = b, _2 = c } }
                    }
            , tensor : ../../Functor/Pair/Type vObject object v base cat.product
            }
          ⩓ ../Type object v base