let cat = ../Category/Cat/semigroupal

let vObject = Type

let Set =
      ../Category/Monoidal/Cartesian/extractMonoidal
        cat
        vObject
        Type
        ../Category/Set/monoidal/cartesian

in  λ(a : Type) →
        { unit = λ(_ : {}) → [] : List a
        , product = λ(x : { _1 : List a, _2 : List a }) → x._1 # x._2
        }
      : ../Monoid/Type Type Set (List a)