Homotopy Type Theory Archimedean ordered abelian group > history (Rev #3, changes)

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

Definition

Given an ordered abelian group AA, let us inductively define the left action act:×AAact:\mathbb{N} \times A \to A as

act(0,a)aact(0, a) \coloneqq a
act(s(n),a)act(n,a)+aact(s(n), a) \coloneqq act(n, a) + a

With strict order

AA is an Archimedean ordered abelian group if there is a family of dependent terms

a:A,b:Aα(a,b):((0<a)×(0<b)) n:a<act(n,b)a:A, b:A \vdash \alpha(a, b): ((0 \lt a) \times (0 \lt b)) \to \Vert \sum_{n:\mathbb{N}} a \lt act(n, b) \Vert

With positivity

AA is an Archimedean ordered abelian group if there is a family of dependent terms

a:A,b:Aα(a,b):(isPositive(a)×isPositive(b)) n:a<act(n,b)a:A, b:A \vdash \alpha(a, b): (\mathrm{isPositive}(a) \times \mathrm{isPositive}(b)) \to \Vert \sum_{n:\mathbb{N}} a \lt act(n, b) \Vert

Examples

See also

Revision on June 15, 2022 at 22:28:30 by Anonymous?. See the history of this page for a list of all contributions to it.