let cat = ../../Category/Cat/semigroupal

let vObject = Type

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

in  λ(m : Type) →
    λ(ring : ./Type m) →
        { additive =
            ../../Group/PartiallyOrderedCommutative/extractCommutativeGroup
              m
              ring.additive
        , multiplicative = ring.multiplicative
        }
      : ../Type Type Set m