Definition
A monoid consists of
- A type ,
- A basepoint
- A binary operation
- A left unitor contractor
- A right unitor contractor
- An asssociator contractor
- A 0-truncator
Properties
Homomorphisms of monoids
A homomorphism of monoids between two monoids and consists of
- A function such that
- The basepoint is preserved
- The binary operation is preserved
For any function
the left unitor contractor is preserved:
because
is contractible. Likewise, for any function
the right unitor contractor is preserved:
because
is contractible, and for any function
the associator contractor is preserved:
because
is contractible. Finally, the 0-truncator is always preserved in a function between two sets.
Relation to -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, and associator respectively, which means that a monoid is an $A_3$-space.
Similarly, any 0-truncated -space or -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 an -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 -space is a monoid.
As monoids are -spaces, given monoids and , for any function
the left unitor is preserved:
because
is contractible. Likewise, for any function
the right unitor is preserved:
because
is contractible, and for any function
the associator is preserved:
because
is contractible. This means that a homomorphism of monoids is also a homomorphism of -spaces.
Examples
-
The integers are a monoid.
-
Given a set , the type of endofunctions has the structure of an monoid, with basepoint , operation function composition.
See also
References