{-|
Every rig category has an additional family of “separator”-based monoidal
structures. That is, for any object `s` there is a generalization of the
additive monoidal structure:

> (a ⊗ s ⊗ b) ⊕ a ⊕ b

When `s` is the additive unit, this structure is isomorphic to the additive
product.
-}
let kCat = ../Cat/semigroupal

in  λ(vObject : Kind) →
    λ(object : Kind) →
    λ(cat : ./Kind kCat vObject object) →
    λ(s : object) →
      let mult = cat.multiplicative.product

      let add = cat.additive.product

      in    { constraint = cat.constraint
            , arrow = cat.arrow
            , product =
                λ(a : kCat.product object object) →
                  add
                    { _1 =
                        add
                          { _1 =
                              mult
                                { _1 = mult { _1 = a._1, _2 = s }, _2 = a._2 }
                          , _2 = a._1
                          }
                    , _2 = a._2
                    }
            , unit = cat.additive.unit
            }
          : ../Monoidal/Kind kCat vObject object