{-|
Should use ../Monoid/Commutative/Monus/Type, but `monus` is complicated with
recursion, so need to figure out how dada ties into this.
-}
let cat = ../Category/Cat/semigroupal

let vObject = Type

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

in    { unit = λ(_ : {}) → 0
      , product = λ(t : { _1 : Natural, _2 : Natural }) → t._1 + t._2
      }
    : ../Monoid/Commutative/Type Type Set Natural