{-|

**TODO**: Ideally, the diamond and star 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 diamond = ./extractDiamond kCat vObject object cat

      let star = ./extractStar kCat vObject object cat

      in    { swap :
                ∀(a : object) →
                ∀(b : object) →
                ∀(c : object) →
                ∀(d : object) →
                  cat.arrow
                    { _1 =
                        diamond.product
                          { _1 = star.product { _1 = a, _2 = b }
                          , _2 = star.product { _1 = c, _2 = d }
                          }
                    , _2 =
                        star.product
                          { _1 = diamond.product { _1 = a, _2 = c }
                          , _2 = diamond.product { _1 = b, _2 = d }
                          }
                    }
            , split :
                cat.arrow
                  { _1 = diamond.unit
                  , _2 = star.product { _1 = diamond.unit, _2 = diamond.unit }
                  }
            , combine :
                cat.arrow
                  { _1 = diamond.product { _1 = star.unit, _2 = star.unit }
                  , _2 = star.unit
                  }
            , switch : cat.arrow { _1 = diamond.unit, _2 = star.unit }
            , diamond : ../Monoidal/Type object v diamond
            , star : ../Monoidal/Type object v star
            }
          ⩓ ../Type object v (./extractCategory kCat vObject object cat)