let kCat = ../Category/Cat/semigroupal

let vObject = Type

let object = Type

let cat =
      ../Category/Monoidal/Cartesian/extractSemigroupal
        kCat
        vObject
        object
        ../Category/Set/monoidal/cartesian

in  λ(m : object) →
    λ(eq : ../Eq/Type m) →
    λ(semigroup : ./Type object cat m) →
      { associativity =
          λ(a : m) →
          λ(b : m) →
          λ(c : m) →
            eq.eq
              ( semigroup.product
                  { _1 = semigroup.product { _1 = a, _2 = b }, _2 = c }
              )
              ( semigroup.product
                  { _1 = a, _2 = semigroup.product { _1 = b, _2 = c } }
              )
      }