{-|

**TODO**: Ideally, the additive and multiplicative monoids shouldn’t _also_ have
the category members (as they just duplicate the ones on the rig), but it was
more trouble to avoid them for the time being.
-}
let kCat = ../Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../Monoidal/Kind kCat Type vObject) →
    λ(cat : ./Kind kCat vObject object) →
      let Isomorphism =
            ../../Isomorphism/Type
              object
              (./extractCategory kCat vObject object cat)

      let additive = ./extractAdditive kCat vObject object cat

      let multiplicative = ./extractMultiplicative kCat vObject object cat

      in    { distributivity :
                ∀(a : object) →
                ∀(b : object) →
                ∀(c : object) →
                  Isomorphism
                    { _1 =
                        multiplicative.product
                          { _1 = a, _2 = additive.product { _1 = b, _2 = c } }
                    , _2 =
                        additive.product
                          { _1 = multiplicative.product { _1 = a, _2 = b }
                          , _2 = multiplicative.product { _1 = a, _2 = c }
                          }
                    }
            , leftAnnihilation :
                ∀(a : object) →
                  Isomorphism
                    { _1 = multiplicative.product { _1 = additive.unit, _2 = a }
                    , _2 = additive.unit
                    }
            , rightAnnihilation :
                ∀(a : object) →
                  Isomorphism
                    { _1 = multiplicative.product { _1 = a, _2 = additive.unit }
                    , _2 = additive.unit
                    }
            , additive : ../Monoidal/Type object v additive
            , multiplicative : ../Monoidal/Type object v multiplicative
            }
          ⩓ ../Type object v (./extractCategory kCat vObject object cat)