{-|
Every monoid in a cartesian category is a bimonoid in a unique way.
-}
let kCat = ../Cat/semigroupal

let Bimonoid = ../../Bimonoid/Type

let CartesianCategory = ./Type

let Monoid = ../../Monoid/Type

let MonoidalCategory = ../Monoidal/Kind kCat

let vObject = Type

in  λ(object : Kind) →
    λ(v : MonoidalCategory Type vObject) →
    λ(cat : MonoidalCategory vObject object) →
    λ(m : object) →
    λ(cartesian : CartesianCategory object v cat m) →
    λ(monoid : Monoid object cat m) →
      { monoid, comonoid = cartesian.comonoid } : Bimonoid object cat m