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

let CartesianCategory = ./Type

let Group = ../../Group/Type

let extractMonoid = ../../Group/extractMonoid

let HopfMonoid = ../../Monoid/Hopf/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) →
    λ(group : Group object cat m) →
          { antipode = group.inverse }
        ∧ ./impliedBimonoid
            object
            v
            cat
            m
            cartesian
            (extractMonoid object cat m group)
      : HopfMonoid object cat m