Homotopy Type Theory
integers > history (Rev #18, changes)
Showing changes from revision #17 to #18:
Added | Removed | Changed
Contents
< integer
Idea
The integers as familiar from school mathematics.
Definitions
The type of integers , denoted ℤ \mathbb{Z} , has several definitions as a higher inductive type .
Definition 1
The integers are defined as the higher inductive type generated by:
A function inj : 2 × ℕ → ℤ inj : \mathbf{2} \times \mathbb{N} \rightarrow \mathbb{Z} .
An identity representing that positive and negative zero are equal: ν 0 : inj ( 0 , 0 ) = inj ( 1 , 0 ) \nu_0: inj(0, 0) = inj(1, 0) .
Definition 2
The integers are defined as the higher inductive type generated by:
A term 0 : ℤ 0 : \mathbb{Z} .
A function s : ℤ → ℤ s : \mathbb{Z} \to \mathbb{Z} .
A function p 1 : ℤ → ℤ p_1 : \mathbb{Z} \to \mathbb{Z} .
A function p 2 : ℤ → ℤ p_2 : \mathbb{Z} \to \mathbb{Z} .
A dependent product of identities representing that p 1 p_1 is a section of s s :σ : ∏ a : ℤ p 1 ( s ( a ) ) = a \sigma: \prod_{a:\mathbb{Z}} p_1(s(a)) = a
A dependent product of identities representing that p 2 p_2 is a retracion of s s :ρ : ∏ a : ℤ s ( p 2 ( a ) ) = a \rho: \prod_{a:\mathbb{Z}} s(p_2(a)) = a
Definition 3
The integers are defined as the higher inductive type generated by:
A term 0 : ℤ 0 : \mathbb{Z} .
A function s : ℤ → ℤ s : \mathbb{Z} \to \mathbb{Z} .
A function p : ℤ → ℤ p : \mathbb{Z} \to \mathbb{Z} .
A dependent product of identities representing that p p is a section of s s :σ : ∏ a : ℤ p ( s ( a ) ) = a \sigma: \prod_{a:\mathbb{Z}} p(s(a)) = a
A dependent product of identities representing that p p is a retracion of s s :ρ : ∏ a : ℤ s ( p ( a ) ) = a \rho: \prod_{a:\mathbb{Z}} s(p(a)) = a
A dependent product of identities representing the coherence condition:κ : ∏ a : ℤ ap s ( σ ( a ) ) = ρ ( a ) \kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)
Definition 4
The integers are defined as the higher inductive type generated by:
A term 0 : ℤ 0 : \mathbb{Z} .
A function s : ℤ → ℤ s : \mathbb{Z} \to \mathbb{Z} .
A function n : ℤ → ℤ n : \mathbb{Z} \to \mathbb{Z} .
An identity representing that zero and negative zero are equal: ν : n ( 0 ) = 0 \nu: n(0) = 0 .
A dependent product of identities representing that negation is an involution:ι : ∏ a : ℤ n ( n ( a ) ) = a \iota: \prod_{a:\mathbb{Z}} n(n(a)) = a
A dependent product of identities representing the coherence condition for the above:κ ι : ∏ a : ℤ ap n ( ι ( a ) ) = ι ( a ) \kappa_\iota: \prod_{a:\mathbb{Z}} ap_n(\iota(a)) = \iota(a)
A dependent product of identities representing that n ∘ s ∘ n n \circ s \circ n is a section of s s :σ : ∏ a : ℤ n ( s ( n ( s ( a ) ) ) ) = a \sigma: \prod_{a:\mathbb{Z}} n(s(n(s(a)))) = a
A dependent product of identities representing that n ∘ s ∘ n n \circ s \circ n is a retracion of s s :ρ : ∏ a : ℤ s ( n ( s ( n ( a ) ) ) ) = a \rho: \prod_{a:\mathbb{Z}} s(n(s(n(a)))) = a
A dependent product of identities representing the coherence condition:κ : ∏ a : ℤ ap s ( σ ( a ) ) = ρ ( a ) \kappa: \prod_{a:\mathbb{Z}} ap_s(\sigma(a)) = \rho(a)
Definition 5
The integers are defined as the higher inductive type generated by:
A function inj : ℕ × ℕ → ℤ inj : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{Z} .
A dependent product of functions between identities representing that equivalent differences are equal:equivdiff : ∏ a : ℕ ∏ b : ℕ ∏ c : ℕ ∏ d : ℕ ( a + d = c + b ) → ( inj ( a , b ) = inj ( c , d ) ) equivdiff : \prod_{a:\mathbb{N}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{N}} \prod_{d:\mathbb{N}} (a + d = c + b) \to (inj(a,b) = inj(c,d))
A set-truncatorτ 0 : ∏ a : ℤ ∏ b : ℤ isProp ( a = b ) \tau_0: \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} isProp(a=b)
Properties
TODO: Show that the integers are a ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the integers are initial in the category of ordered Heyting integral domains.
We assume in this section that the integers are defined according to definition 1.
Commutative ring structure on the integers
Definition
The integer zero 0 : ℤ 0:\mathbb{Z} is defined as
0 ≔ inj ( 0 , 0 ) 0 \coloneqq inj(0, 0)
Definition
Let ( − ) + ( − ) : ℕ × ℕ → ℕ (-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N} be addition of the natural numbers, let ρ : ℕ × ℕ → ℕ \rho:\mathbb{N} \times \mathbb{N} \to \mathbb{N} be the symmetric difference or metric of the natural numbers, and let < : ℕ × ℕ → 𝟚 \lt:\mathbb{N} \times \mathbb{N} \to \mathbb{2} be the decidable strict order on the natural numbers into the booleans. The binary operation addition ( − ) + ( − ) : ℤ × ℤ → ℤ (-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is inductively defined as
inj ( 0 , a ) + inj ( 0 , b ) ≔ inj ( 0 , a + b ) inj(0,a) + inj(0,b) \coloneqq inj(0,a+b) inj ( 1 , a ) + inj ( 1 , b ) ≔ inj ( 1 , a + b ) inj(1,a) + inj(1,b) \coloneqq inj(1,a+b) inj ( 0 , a ) + inj ( 1 , b ) ≔ inj ( a < b , ρ ( a , b ) ) inj(0,a) + inj(1,b) \coloneqq inj(a \lt b,\rho(a,b)) inj ( 1 , a ) + inj ( 0 , b ) ≔ inj ( b < a , ρ ( a , b ) ) inj(1,a) + inj(0,b) \coloneqq inj(b \lt a,\rho(a,b))
for a : ℕ a:\mathbb{N} , b : ℕ b:\mathbb{N} .
Definition
The unary operation negation − ( − ) : ℤ → ℤ -(-):\mathbb{Z} \to \mathbb{Z} is defined as
− inj ( a , b ) ≔ inj ( ¬ a , b ) -inj(a, b) \coloneqq inj(\neg a, b)
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , ¬ : 2 → 2 \neg:\mathbf{2} \to \mathbf{2}
Definition
The binary operation subtraction ( − ) − ( − ) : ℤ × ℤ → ℤ (-)-(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as
inj ( a , b ) − inj ( c , d ) ≔ inj ( a , b ) + inj ( ¬ c , d ) inj(a, b) - inj(c, d) \coloneqq inj(a, b) + inj(\neg c, d)
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The integer number one 1 : ℤ 1:\mathbb{Z} is defined as
1 ≔ inj ( 0 , 1 ) 1 \coloneqq inj(0,1)
Definition
The binary operation multiplication ( − ) ⋅ ( − ) : ℤ × ℤ → ℤ (-)\cdot(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as
inj ( a , b ) ⋅ inj ( c , d ) ≔ inj ( a ⊕ c , b ⋅ d ) inj(a,b) \cdot inj(c,d) \coloneqq inj(a \oplus c,b \cdot d)
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} , ( − ) ⋅ ( − ) : ℕ × ℕ → ℕ (-)\cdot(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N} , ( − ) ⊕ ( − ) : 2 × 2 → 2 (-)\oplus(-):\mathbf{2} \times \mathbf{2} \to \mathbf{2} (exclusive or binary operation in 2 \mathbf{2} ).
Definition
The right ℕ \mathbb{N} -action exponentiation ( − ) ( − ) : ℤ × ℕ → ℤ (-)^{(-)}:\mathbb{Z} \times \mathbb{N} \to \mathbb{Z} is inductively defined as
inj ( a , b ) 0 ≔ inj ( 0 , 1 ) inj(a,b)^0 \coloneqq inj(0,1) inj ( a , b ) 2 n ≔ inj ( 0 , b 2 n ) inj(a,b)^{2n} \coloneqq inj(0,b^{2n}) inj ( a , b ) 2 n + 1 ≔ inj ( a , b 2 n + 1 ) inj(a,b)^{2n+1} \coloneqq inj(a,b^{2n+1})
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , n : ℕ n:\mathbb{N} , ( − ) ( − ) : ℕ × ℕ → ℕ (-)^{(-)}:\mathbb{N} \times \mathbb{N} \to \mathbb{N} .
Order structure on the integers
Definition
The dependent type is positive , denoted as isPositive ( inj ( a , b ) ) isPositive(inj(a,b)) , is defined as
isPositive ( inj ( a , b ) ) ≔ ( a = 0 ) × ( b > 0 ) isPositive(inj(a,b)) \coloneqq (a = 0) \times (b \gt 0)
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , dependent types m > n m\gt n indexed by m , n : ℕ m, n:\mathbb{N} .
Definition
The dependent type is negative , denoted as isNegative ( inj ( a , b ) ) isNegative(inj(a,b)) , is defined as
isPositive ( inj ( a , b ) ) ≔ ( a = 1 ) × ( b > 0 ) isPositive(inj(a,b)) \coloneqq (a = 1) \times (b \gt 0)
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , dependent types m > n m\gt n indexed by m , n : ℕ m, n:\mathbb{N} .
Definition
The dependent type is zero , denoted as isZero ( inj ( a , b ) ) isZero(inj(a,b)) , is defined as
isZero ( inj ( a , b ) ) ≔ b = 0 isZero(inj(a,b)) \coloneqq b = 0
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} .
Definition
The dependent type is non-positive , denoted as isNonPositive ( inj ( a , b ) ) isNonPositive(inj(a,b)) is defined as
isNonPositive ( inj ( a , b ) ) ≔ isPositive ( inj ( a , b ) ) → ∅ isNonPositive(inj(a,b)) \coloneqq isPositive(inj(a,b)) \to \emptyset
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} .
Definition
The dependent type is non-negative , denoted as isNonNegative ( inj ( a , b ) ) isNonNegative(inj(a,b)) , is defined as
isNonNegative ( inj ( a , b ) ) ≔ isNegative ( inj ( a , b ) ) → ∅ isNonNegative(inj(a,b)) \coloneqq isNegative(inj(a,b)) \to \emptyset
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} .
Definition
The dependent type is non-zero , denoted as isNonZero ( inj ( a , b ) ) isNonZero(inj(a,b)) , is defined as
isNonZero ( inj ( a , b ) ) ≔ ‖ isPositive ( inj ( a , b ) ) + isNegative ( inj ( a , b ) ) ‖ isNonZero(inj(a,b)) \coloneqq \Vert isPositive(inj(a,b)) + isNegative(inj(a,b)) \Vert
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} .
Definition
The dependent type is less than , denoted as inj ( a , b ) < inj ( c , d ) inj(a,b) \lt inj(c,d) , is defined as
inj ( a , b ) < inj ( c , d ) ≔ isPositive ( inj ( c , d ) − inj ( a , b ) ) inj(a,b) \lt inj(c,d) \coloneqq isPositive(inj(c,d) - inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The dependent type is greater than , denoted as inj ( a , b ) > inj ( c , d ) inj(a,b) \gt inj(c,d) , is defined as
inj ( a , b ) > inj ( c , d ) ≔ isNegative ( inj ( c , d ) − inj ( a , b ) ) inj(a,b) \gt inj(c,d) \coloneqq isNegative(inj(c,d) - inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The dependent type is apart from , denoted as inj ( a , b ) # inj ( c , d ) inj(a,b) # inj(c,d) , is defined as
inj ( a , b ) # inj ( c , d ) ≔ isNonZero ( inj ( c , d ) − inj ( a , b ) ) inj(a,b) # inj(c,d) \coloneqq isNonZero(inj(c,d) - inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The dependent type is less than or equal to , denoted as inj ( a , b ) ≤ inj ( c , d ) inj(a,b) \leq inj(c,d) , is defined as
inj ( a , b ) ≤ inj ( c , d ) ≔ isNonNegaitve ( inj ( c , d ) − inj ( a , b ) ) inj(a,b) \leq inj(c,d) \coloneqq isNonNegaitve(inj(c,d) - inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The dependent type is greater than or equal to , denoted as inj ( a , b ) ≥ inj ( c , d ) inj(a,b) \geq inj(c,d) , is defined as
inj ( a , b ) ≥ inj ( c , d ) ≔ isNonPositive ( inj ( c , d ) − inj ( a , b ) ) inj(a,b) \geq inj(c,d) \coloneqq isNonPositive(inj(c,d) - inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Pseudolattice structure on the integers
Definition
The ramp function ramp : ℤ → ℤ ramp:\mathbb{Z} \to \mathbb{Z} is inductively defined as
ramp ( inj ( 0 , a ) ) ≔ inj ( 0 , a ) ramp(inj(0, a)) \coloneqq inj(0, a) ramp ( inj ( 1 , a ) ) ≔ 0 ramp(inj(1, a)) \coloneqq 0
for a : ℕ a:\mathbb{N} .
Definition
The minimum min : ℤ × ℤ → ℤ min:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as
min ( inj ( a , b ) , inj ( c , d ) ) ≔ inj ( a , b ) − ramp ( inj ( a , b ) − inj ( c , d ) ) min(inj(a,b),inj(c,d)) \coloneqq inj(a,b) - ramp(inj(a,b) - inj(c,d))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The maximum max : ℤ × ℤ → ℤ max:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as
max ( inj ( a , b ) , inj ( c , d ) ) ≔ inj ( a , b ) + ramp ( inj ( c , d ) − inj ( a , b ) ) max(inj(a,b),inj(c,d)) \coloneqq inj(a,b) + ramp(inj(c,d) - inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} , c : 2 c:\mathbf{2} , d : ℕ d:\mathbb{N} .
Definition
The absolute value | ( − ) | : ℤ → ℤ \vert(-)\vert:\mathbb{Z} \to \mathbb{Z} is defined as
| inj ( a , b ) | ≔ max ( inj ( a , b ) , − inj ( a , b ) ) \vert inj(a,b) \vert \coloneqq max(inj(a,b), -inj(a,b))
for a : 2 a:\mathbf{2} , b : ℕ b:\mathbb{N} .
Division and remainder
Definition
Integer division ( − ) ÷ ( − ) : ℤ × ℤ ≠ 0 → ℤ (-)\div(-):\mathbb{Z} \times \mathbb{Z}_{\neq 0} \to \mathbb{Z} is defined as
inj ( 0 , a ) ÷ inj ( 0 , b ) ≔ inj ( 0 , a ÷ b ) inj(0,a) \div inj(0,b) \coloneqq inj(0,a \div b) inj ( 0 , a ) ÷ inj ( 1 , b ) ≔ inj ( 1 , a ÷ b ) inj(0,a) \div inj(1,b) \coloneqq inj(1,a \div b) inj ( 1 , a ) ÷ inj ( 0 , b ) ≔ inj ( 1 , a ÷ b ) inj(1,a) \div inj(0,b) \coloneqq inj(1,a \div b) inj ( 1 , a ) ÷ inj ( 1 , b ) ≔ inj ( 0 , a ÷ b ) inj(1,a) \div inj(1,b) \coloneqq inj(0,a \div b)
for a : ℕ a:\mathbb{N} , b : ℕ ≠ 0 b:\mathbb{N}_{\neq 0} .
Properties
The integers are sequentially Cauchy complete with respect to the distance function defined as d ( x , y ) ≔ | x − y | d(x, y) \coloneqq \vert x - y \vert . This is because any Cauchy sequence in the integers converges to an integer n n and only has a finite number of terms that are not equal to n n . This is because the integers are not dense.
See also
References
Revision on June 17, 2022 at 18:15:40 by
Anonymous? .
See the history of this page for a list of all contributions to it.