Homotopy Type Theory
monoid > history (Rev #1)
Definition
A monoid consists of
- A type ,
- A basepoint
- A binary operation
- A left unitor
- A right unitor
- An asssociator
- A 0-truncator
Examples
-
The integers are a monoid.
-
Every loop space is naturally a monoid with path concatenation as the operation. In fact every loop space is a group.
-
Given a set , the type of endofunctions has the structure of an monoid, with basepoint , operation function composition.
See also
Revision on February 3, 2022 at 23:53:31 by
Anonymous?.
See the history of this page for a list of all contributions to it.