Showing changes from revision #3 to #4:
Added | Removed | Changed
Definition
A commutative monoid or commutative -algebra in sets consists of
- A type ,
- A basepoint
- A binary operation
- A left unitor contractor
- A right unitor contractor
- An asssociator contractor
- A commutator contractor
- 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