let kCat = ../../../Category/Cat/semigroupal

let Set = ../../../Category/Set/rig

let vObject = Type

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

let object = Type

let cat = ../../../Category/Rig/extractMultiplicative kCat vObject object Set

let Semigroup =
      ../../../Semigroup/Type
        object
        (../../../Category/Monoidal/extractSemigroupal kCat vObject object cat)

in  λ(a : object) →
    λ(semigroup : Semigroup a) →
          ../endo/star
            (../../../Identity/Type object)
            ../../../Identity/functor/monoidal
            a
        ∧ { unit =
              λ(b : object) →
              λ(fn : Set.arrow { _1 = Set.multiplicative.unit, _2 = b }) →
                (Set.additive.product { _1 = a, _2 = b }).Right (fn {=})
          , product =
              λ(i : object) →
              λ ( day
                : ∀(r : Type) →
                  ( ∀(d : { _1 : object, _2 : object }) →
                    Set.arrow { _1 = Set.multiplicative.product d, _2 = i } →
                    { _1 : Set.additive.product { _1 = a, _2 = d._1 }
                    , _2 : Set.additive.product { _1 = a, _2 = d._2 }
                    } →
                      r
                  ) →
                    r
                ) →
                day
                  (Set.additive.product { _1 = a, _2 = i })
                  ( λ(p : { _1 : object, _2 : object }) →
                    λ ( fn
                      : Set.arrow { _1 = Set.multiplicative.product p, _2 = i }
                      ) →
                    λ ( args
                      : { _1 : Set.additive.product { _1 = a, _2 = p._1 }
                        , _2 : Set.additive.product { _1 = a, _2 = p._2 }
                        }
                      ) →
                      merge
                        { Left =
                            λ(l : a) →
                              merge
                                { Left =
                                    λ(ll : a) →
                                      ( Set.additive.product { _1 = a, _2 = i }
                                      ).Left
                                        (semigroup.product { _1 = l, _2 = ll })
                                , Right =
                                    λ(_ : p._2) →
                                      ( Set.additive.product { _1 = a, _2 = i }
                                      ).Left
                                        l
                                }
                                args._2
                        , Right =
                            λ(f : Set.arrow { _1 = p._2, _2 = i }) →
                              merge
                                { Left =
                                    ( Set.additive.product { _1 = a, _2 = i }
                                    ).Left
                                , Right =
                                    λ(x : p._2) →
                                      ( Set.additive.product { _1 = a, _2 = i }
                                      ).Right
                                        (f x)
                                }
                                args._2
                        }
                        ( merge
                            { Left =
                                ( Set.additive.product { _1 = a, _2 = p._2 → i }
                                ).Left
                            , Right =
                                λ(x : p._1) →
                                  ( Set.additive.product
                                      { _1 = a, _2 = p._2 → i }
                                  ).Right
                                    (λ(y : p._2) → fn { _1 = x, _2 = y })
                            }
                            args._1
                        )
                  )
          }
      : ../../../Functor/Monoidal/Type
          object
          v
          cat
          cat
          (λ(b : object) → Set.additive.product { _1 = a, _2 = b })