Homotopy Type Theory an axiomatization of the real numbers > history (Rev #12, changes)

Showing changes from revision #11 to #12: Added | Removed | Changed

Contents

Definition

Propositions

A proposition is a type AA with an identification p:a= Abp:a =_A b for all elements a:Aa:A and b:Ab:A.

Sets

A set is a type AA such that for all elements a:Aa:A and b:Ab:A, the identity type a= Aba =_A b is a proposition.

Pointed abelian groups

A pointed abelian group is a set AA with an element 1:A1:A called one and a binary operation ()():A×AA(-)-(-):A \times A \to A called subtraction such that

  • for all elements a:Aa:A, aa=11a - a = 1 - 1

  • for all elements a:Aa:A, (11)((11)a)=a(1 - 1) - ((1 - 1) - a) = a

  • for all elements a:Aa:A and b:Ab:A, a((11)b)=b((11)a)a - ((1 - 1) - b) = b - ((1 - 1) - a)

  • for all elements a:Aa:A, b:Ab:A, and c:Ac:A, a(bc)=(a((11)c))ba - (b - c) = (a - ((1 - 1) - c)) - b

Pointed halving groups

A pointed halving group is a pointed abelian group G with a function ()/2:GG(-)/2:G \to G called halving or dividing by two such that for all elements g:Gg:G, g/2=gg/2g/2 = g - g/2.

Totally ordered pointed halving groups

A pointed halving group RR is a totally ordered pointed halving group if it comes with a function max:R×RR\max:R \times R \to R such that

  • for all elements a:Ra:R, max(a,a)=a\max(a, a) = a

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=max(b,a)\max(a, b) = \max(b, a)

  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, max(a,max(b,c))=max(max(a,b),c)\max(a, \max(b, c)) = \max(\max(a, b), c)

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=a\max(a, b) = a or max(a,b)=b\max(a, b) = b

  • for all elements a:Ra:R and b:Rb:R, max(a,b)=b\max(a, b) = b implies that for all elements c:Rc:R, max(ac,bc)=bc\max(a - c, b - c) = b - c

Strictly ordered pointed halving groups

A totally ordered pointed halving group RR is a strictly ordered pointed abelian group if it comes with a type family <\lt such that

  • for all elements a:Ra:R and b:Rb:R, a<ba \lt b is a proposition
  • for all elements a:Ra:R, a<aa \lt a is false
  • for all elements a:Ra:R, b:Rb:R, and c:Rc:R, if a<ca \lt c, then a<ba \lt b or b<cb \lt c
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b is false and b<ab \lt a is false, then a=ba = b
  • for all elements a:Ra:R and b:Rb:R, if a<ba \lt b, then b<ab \lt a is false.
  • 11<11 - 1 \lt 1
  • for all elements a:Ra:R and b:Rb:R, if 11<a1 - 1 \lt a and 11<b1 - 1 \lt b, then (11)<a((11)b)(1 - 1) \lt a - ((1 - 1) - b)

The homotopy initial strictly ordered pointed halving group is the dyadic rational numbers𝔻\mathbb{D}.

Archimedean ordered pointed halving groups

A strictly ordered pointed halving group AA is an Archimedean ordered pointed halving group if for all elements a:Aa:A and b:Ab:A, if a<ba \lt b, then there merely exists a dyadic rational number d:𝔻d:\mathbb{D} such that a<h(d)a \lt h(d) and h(d)<bh(d) \lt b.

Sequentially Cauchy complete Archimedean ordered pointed halving groups

Let AA be an Archimedean ordered pointed halving group and let

A + a:A11<aA_{+} \coloneqq \sum_{a:A} 1 - 1 \lt a

be the positive elements in AA.

A sequence in AA is a function x:Ax:\mathbb{N} \to A.

A sequence x:Ax:\mathbb{N} \to A is a Cauchy sequence if for all positive elements ϵ:A +\epsilon:A_{+}, there merely exists a natural number N:N:\mathbb{N} such that for all natural numbers i:i:\mathbb{N} and j:j:\mathbb{N} such that NiN \leq i and NjN \leq j, max(x ix j,x jx i)<ϵ\max(x_i - x_j, x_j - x_i) \lt \epsilon.

An element l:Al:A is said to be a limit of the sequence x:Ax:\mathbb{N} \to A if for all positive elements ϵ:A +\epsilon:A_{+}, there merely exists a natural number N:N:\mathbb{N} such that for all natural numbers i:i:\mathbb{N} such that NiN \leq i, max(x il,lx i)<ϵ\max(x_i - l, l - x_i) \lt \epsilon

AA is sequentially Cauchy complete if every Cauchy sequence in AA merely has a limit.

Revision on June 19, 2022 at 03:05:24 by Anonymous?. See the history of this page for a list of all contributions to it.