Bimonoid object
Category of bimonoid objects
The category of bimonoids in , denoted , is a category where
an object is a bimonoid object in
and a morphism is a bimonoid morphism. #m/def/cat
We therefore have isomorphisms of categories
where we invoke and .
As the bicartesian completion of a symmetric monoidal category
If is a symmetric monoidal category then the tensor product of two bimonoids in naturally carries the structure of a bimonoid.
- By the above isomorphism, we have the following diamond of forgetful functors
which are all monoidal if is symmetric.
#state/tidy | #lang/en | #SemBr