Showing changes from revision #7 to #8:
Added | Removed | Changed
Definition
A commutative monoid consists of
- A type ,
- A basepoint
- A binary operation
- A contractible left unit identity
- A contractible right unit identity
- A contractible associative identity
- A contractible commutative identity
- A 0-truncator
Properties
Relation to commutative -spaces
Since for all , , , , and are contractible, the types
are contractible and thus pointed, and thus one could choose any point
to be the left unitor, right unitor, associator, and commutator respectively, which means that a commutative monoid is a commutative $A_3$-space.
Similarly, any 0-truncated commutative -space or commutative -algebra in sets is a monoid, as any identity type between any two terms of a set are propositions, and thus for every , the identity types , , , and are propositions. Since the dependent product types
are inhabited by definition of a commutative -space, each identity type , , , and is an inhabited proposition, which makes it contractible. Thus,
which along with the 0-truncator means that a 0-truncated commutative -space is a commutative monoid.
Examples
See also