{-|

**TODO**: Should be a Rig/Commutative
-}
let cat = ../Category/Cat/semigroupal

let vObject = Type

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

in    { additive =
        { unit = λ(_ : {}) → 0
        , product = λ(t : { _1 : Natural, _2 : Natural }) → t._1 + t._2
        }
      , multiplicative =
        { unit = λ(_ : {}) → 1
        , product = λ(t : { _1 : Natural, _2 : Natural }) → t._1 * t._2
        }
      }
    : ../Rig/Type Type Set Natural