let kCat = ../Category/Cat/semigroupal

let vObject = Type

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

in  λ(object : Kind) →
    λ(cat : ../Category/Monoidal/Kind kCat vObject object) →
    λ(category : ../Category/Monoidal/Type object v cat) →
    λ(m : object) →
    λ(group : ./Type object cat m) →
      let base = ../Category/Monoidal/extractCategory kCat vObject object cat

      in  category.product
            { _1 = cat.product { _1 = m, _2 = m }, _2 = m }
            ( λ(r : Type) →
              λ ( arrowsOut
                : ∀(z : object) →
                  cat.arrow { _1 = z, _2 = m } →
                  cat.arrow { _1 = cat.product { _1 = m, _2 = m }, _2 = z } →
                    r
                ) →
                arrowsOut
                  (cat.product { _1 = m, _2 = m })
                  group.product
                  ( ( ../Functor/Bifunctor/impliedSecondFunctor
                        object
                        base
                        ( ../Category/Monoidal/extractCategoryInstance
                            object
                            v
                            cat
                            category
                        )
                        object
                        base
                        object
                        base
                        cat.product
                        category.tensor
                        m
                    ).map
                      m
                      m
                      group.inverse
                  )
            )