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

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

Contents

Definition

Abelian Propositions groups

An A abelian proposition group is a pointed type set(A,0) (A, A 0) with a an binary identification operation(p)(): A a×= A A bA (-)-(-):A p:a \times =_A A b \to A called for all elementssubtractiona:Aa:A such and thatb:Ab:A.

  • for all aAa \in A, aa=0a - a = 0

  • for all aAa \in A, 0(0a)=a0 - (0 - a) = a

  • for all aAa \in A and bAb \in A, a(0b)=b(0a)a - (0 - b) = b - (0 - a)

  • for all aAa \in A, bAb \in A, and cAc \in A, a(bc)=(a(0c))ba - (b - c) = (a - (0 - c)) - b

Sets

Halving groups

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.

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

Pointed abelian groups

Totally ordered halving 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

An abelian group RR is a totally ordered abelian group if it comes with a function max:R×RR\max:R \times R \to R 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

  • 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)=b\max(a, b) = b implies that for all elements c:Rc:R, max(ac,bc)=bc\max(a - c, b - c) = 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

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 commutative pointed ring halving groupRR is a strictly ordered pointed abelian group if it comes with an a element type family1<:R 1:R \lt and 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.
  • 0 11<1 0 1 - 1 \lt 1
  • for all elements a:Ra:R and b:Rb:R, if 0 11<a 0 1 - 1 \lt a and 0 11<b 0 1 - 1 \lt b, then 0(11)<a(0(11)b) 0 (1 - 1) \lt a - (0 ((1 - 1) - b)

The 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:A 0 11<a A_{+} \coloneqq \sum_{a:A} 0 1 - 1 \lt a

be the positive elements in AA .AA is sequentially Cauchy complete if every Cauchy sequence in AA converges:

isCauchy(x)ϵA +.NI.iI.jI.(iN)(jN)(|x ix j|<ϵ)isCauchy(x) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (\vert x_i - x_j \vert \lt \epsilon)

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

isLimit(x,l)ϵA +.NI.iI.(iN)(|x il|<ϵ)isLimit(x, l) \coloneqq \forall \epsilon \in A_{+}. \exists N \in I. \forall i \in I. (i \geq N) \to (\vert x_i - l \vert \lt \epsilon)
x:A.isCauchy(x)lA.isLimit(x,l)\forall x: \mathbb{N} \to A. isCauchy(x) \wedge \exists l \in A. isLimit(x, l)

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 17, 2022 at 22:55:40 by Anonymous?. See the history of this page for a list of all contributions to it.