Showing changes from revision #5 to #6:
Added | Removed | Changed
Definition
A monoid or -algebra in sets consists of
A type ,
A basepoint
A binary operation
A left unitor
A right unitor
An asssociator
A 0-truncator
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 monoid , the 0-truncator means that the identity types between any two terms of are propositions, and thus the dependent product typespropositions, and thus the dependent product types
are propositions, and thus contractible because they are inhabited by definition of a monoid.contractible because they are inhabited by definition of a monoid.
As a result, 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. Finally, the 0-truncator is always preserved in a function between two sets.