 Monoid object

ID: monoid-object

m : A \otimes A \to A

and unit

j : I \to A

satisfying associativity and unit diagrams using the ambient associators and unitors.

 New to topics? Read the docs here!