#Contents# * table of contents {:toc} ## Definition ## ### In any magma ### Let $\mathbb{Z}_{+}$ be the type of all positive [[integers]]: $$\mathbb{Z}_{+} \coloneqq \sum_{n:\mathbb{Z}} n \gt 0$$ A __power-associative magma__ consists of * A type $A$, * A binary operation $\mu : A \times A \to A$ * A binary power function ${(-)}^{(-)}: A \times \mathbb{Z}_{+} \to A$ * Two families of dependent terms of identities $$a:A \vdash i(a): a^1 = a$$ $$m:\mathbb{Z}_{+}, n:\mathbb{Z}_{+}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}$$ stating that the power is a right multiplicative $\mathbb{Z}_{+}$-[[action]]. * A family of dependent terms of identities $$a:A, m:\mathbb{Z}_{+}, n:\mathbb{Z}_{+} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}$$ representing the law of exponents for the magma. * A family of dependent terms of identities $$a:A, b:A \vdash \tau_0(a,b):isProp(a=b)$$ representing that $A$ is a [[set]]. The associative and commutative identities for powers of $a:A$ follow from the associative and commutative identities of addition in $\mathbb{Z}_{+}$. ### In a unital magma ### There is a definition of a power-associative unital magma with two-sided inverses, without using explicit unit identites: A __power-associative unital magma__ consists of * A type $A$ * A term $e:A$ * A binary operation $\mu : A \times A \to A$ * A binary power function ${(-)}^{(-)}: A \times \mathbb{N} \to A$ * Two families of dependent terms of identities $$a:A \vdash i(a): a^1 = a$$ $$m:\mathbb{N}, n:\mathbb{N}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}$$ stating that the power is a right multiplicative $\mathbb{N}$-[[action]]. * A family of dependent terms of identities $$a:A \vdash z(a): a^0 = e$$ * A family of dependent terms of identities $$a:A, m:\mathbb{N}, n:\mathbb{N} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}$$ representing the law of exponents for the magma. * A family of dependent terms of identities $$a:A, b:A \vdash \tau_0(a,b):isProp(a=b)$$ representing that $A$ is a [[set]]. The associative, commutative and unit identities for powers of $a:A$ follow from the associative, commutative, and unit identities of addition in $\mathbb{N}$. ### In a magma with two-sided inverses ### There is a definition of a power-associative magma with two-sided inverses, without using explicit inverses as structure or property: A __power-associative magma with two-sided inverses__ consists of * A type $A$, * A binary operation $\mu : A \times A \to A$ * A binary power function ${(-)}^{(-)}: A \times \mathbb{Z} \to A$ * Two families of dependent terms of identities $$a:A \vdash i(a): a^1 = a$$ $$m:\mathbb{Z}, n:\mathbb{Z}, a:A \vdash c(m, n, a): (a^m)^n = a^{m \cdot n}$$ stating that the power is a right multiplicative $\mathbb{Z}$-[[action]]. * A family of dependent terms of identities $$a:A, m:\mathbb{Z}, n:\mathbb{Z} \vdash \pi(a, m, n):\mu(a^m, a^n)=a^{m+n}$$ representing the law of exponents for the magma. * A family of dependent terms of identities $$a:A, b:A \vdash \tau_0(a,b):isProp(a=b)$$ representing that $A$ is a [[set]]. The associative, commutative, and inverse element identities for powers of $a:A$ follow from the associative, commutative, and inverse element identities of addition in $\mathbb{Z}$. In addition, the unit identities for powers of $a:A$ follow as well if $A$ is inhabited. ## See also ## * [[Higher algebra]] * [[monoid]] * [[action]]