Homotopy Type Theory power function > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

< power function

In a

ring AA, multiplication is a power-associative magma, and thus AA has:

  • A binary power function () ():A×A{(-)}^{(-)}: A \times \mathbb{N} \to A
  • Two families of dependent terms of identities
    a:Ai(a):a 1=aa:A \vdash i(a): a^1 = a
    m:,n:,a:Ac(m,n,a):(a m) n=a mnm:\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,m:,n:π(a,m,n):μ(a m,a n)=a m+na: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 multiplicative magma.

See also

Revision on June 13, 2022 at 21:52:35 by Anonymous?. See the history of this page for a list of all contributions to it.