Homotopy Type Theory magma > history (Rev #1)

Definition

A magma is a type $A$ with a binary operation $\mu:A \times A \to A$ and a term $p:isSet(A)$ stating that $A$ is a set.

See also

• monoid
• Z-algebra