Bimonoids

Stream: maths

[Marcus Rossel]

Does Mathlib contain something in the direction of (strong) bimonoids (as described in Section 2.1 in this paper)?
I was considering formalizing some theory of weighted tree automata, which is built upon strong bimonoids.

[Eric Wieser]

Sounds like a bimonoid is [monoid X] [add_monoid X]

[Eric Wieser]

I guess for a strong bimonoid you'd need to make a new class:

set_option old_structure_cmd true

class strong_bimonoid (X : Type*) extends add_comm_monoid_with_one X, monoid_with_zero X.

-- all semiring are strong bimonoids
instance semiring.to_strong_bimonoid (R : Type*) [semiring R] : strong_bimonoid R :=
{ ..‹semiring R› }

(docs#add_comm_monoid_with_one, docs#monoid_with_zero)