Homotopy Type Theory
integers > history (Rev #2)
Contents
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 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 Heyting ordered integral domain with decidable equality, decidable apartness, and decidable linear order, and that the integers are initial in the category of Heyting ordered integral domain.
See also
References
HoTT book
Thorsten Altinkirch, The Integers as a Higher Inductive Type , (abs:2007.00167 )
Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson, Symmetry , (pdf )
Revision on February 26, 2022 at 14:40:55 by
Anonymous? .
See the history of this page for a list of all contributions to it.