nLab integers type

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Deduction and Induction

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

In type theory: the integers type is the type of integers.

Definitions

As the inductive type generated by an element and an equivalence of types

Assuming that identification types, equivalence types and dependent product types exist in the type theory, the integers type is the inductive type generated by an element and an equivalence of types:

Formation rules for the integers type:

ΓctxΓtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{Z} \; \mathrm{type}}

Introduction rules for the integers type:

ΓctxΓ0:ΓctxΓs:\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{Z}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash s:\mathbb{Z} \simeq \mathbb{Z}}

Elimination rules for the integers type:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γind C(c 0,c s,n):C(n)\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x)) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_0, c_s, n):C(n)}

Computation rules for the integers type:

  • Judgmental computation rules
Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γind C(c 0,c s,0)c 0:C(0)\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_0, c_s, 0) \equiv c_0:C(0)}
Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γind C(c 0,c s,s(n))c s(n)(ind C(c 0,c s,n)):C(s(n))\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x)) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c_0, c_s, s(n)) \equiv c_s(n)(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, n)):C(s(n))}
  • Typal computation rules
Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γβ 0(c 0,c s):Id C(0)(ind C(c 0,c s,0),c 0)\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \beta_\mathbb{Z}^0(c_0, c_s):\mathrm{Id}_{C(0)}(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, 0), c_0)}
Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γβ s(c 0,c s,n):Id C(s(n))(ind C(c 0,c s,s(n)),c s(n)(ind C(c 0,c s,n)))\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x)) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \beta_\mathbb{Z}^s(c_0, c_s, n):\mathrm{Id}_{C(s(n))}(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, s(n)), c_s(n)(\mathrm{ind}_\mathbb{Z}^C(c_0, c_s, n)))}

Uniqueness rules for the integers type:

  • Judgmental uniqueness rules
Γ,x:C(x)typeΓc: x:C(x)Γn:Γind C(c(0),λx:.c(s(x)),n)c(n):C(n)\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{Z}} C(x) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \mathrm{ind}_\mathbb{Z}^C(c(0), \lambda x:\mathbb{Z}.c(s(x)), n) \equiv c(n):C(n)}
  • Typal uniqueness rules
Γ,x:C(x)typeΓc: x:C(x)Γn:Γη (c,n):Id C(n)(ind C(c(0),λx:.c(s(x)),n),c(n))\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{Z}} C(x) \quad \Gamma \vdash n:\mathbb{Z}}{\Gamma \vdash \eta_\mathbb{Z}(c, n):\mathrm{Id}_{C(n)}(\mathrm{ind}_\mathbb{Z}^C(c(0), \lambda x:\mathbb{Z}.c(s(x)), n), c(n))}

The elimination, computation, and uniqueness rules for the integers type state that the integers type satisfy the dependent universal property of the integers. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the integers could be simplified to the following rule:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γup C(c 0,c s):!c: x:C(x).Id C(0)(c(0),c 0)× x:Id C(s(x))(c(s(x)),c s(c(x)))\frac{\Gamma, x:\mathbb{Z} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{Z}} C(x) \simeq C(s(x))}{\Gamma \vdash \mathrm{up}_\mathbb{Z}^C(c_0, c_s):\exists!c:\prod_{x:\mathbb{Z}} C(x).\mathrm{Id}_{C(0)}(c(0), c_0) \times \prod_{x:\mathbb{Z}} \mathrm{Id}_{C(s(x))}(c(s(x)), c_s(c(x)))}

As the underlying type of the free infinity-group on the unit type

The integers type is the underlying type of free infinity-group on the unit type

UnderlyingTypeOfFreeGroup(𝟙)\mathbb{Z} \coloneqq \mathrm{UnderlyingTypeOfFree}\infty\mathrm{Group}(\mathbb{1})

As the loop space of the circle type

Given a dependent type theory with identity types, equivalence types, a univalent universe, and the circle type which is an essentially small type relative to the universe universe, the type of integers is defined as the loop space type of the circle type at the canonical element base:S 1\mathrm{base}:S^1:

base= S 1base\mathbb{Z} \coloneqq \mathrm{base} =_{S^1} \mathrm{base}

As a quotient of a product type

Definition

The integers type is 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

The integers type is 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

We assume in this section that the integers type is defined as the inductive type generated by an element and an equivalence of types.

Abelian group structure on the integers

Definition

The binary operation addition is defined by double induction on the integers type

Introduction rules for addition:

ΓctxΓ,x:,y:x+y:\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash x + y:\mathbb{Z}}

Computation rules for addition:

ΓctxΓβ +,0,0:0+0= 0\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{+, 0, 0}:0 + 0 =_\mathbb{Z} 0}
ΓctxΓ,x:β +,0,s(x):0+s(x)= s(0+x)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{+, 0, s}(x):0 + s(x) =_\mathbb{Z} s(0 + x)}
ΓctxΓ,x:β +,s,0(x):s(x)+0= s(x+0)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{+, s, 0}(x):s(x) + 0 =_\mathbb{Z} s(x + 0)}
ΓctxΓ,x:,y:β +,s,s(x,y):s(x)+s(y)= s(s(x+y))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \beta_\mathbb{Z}^{+, s, s}(x, y):s(x) + s(y) =_\mathbb{Z} s(s(x + y))}

Theorem

The integers type is a non-coherent H-space with respect to the zero integer 0:0:\mathbb{Z} found in the introduction rule of the integers type and addition x:,y:x+y:x:\mathbb{Z}, y:\mathbb{Z} \vdash x + y:\mathbb{Z} defined above.

Proof

We define the homotopies for the H-space structure of the integers type by induction on the integers type. For the case with the element 0:0:\mathbb{Z}, one gets the identity β +,0,0:0+0= 0\beta_\mathbb{Z}^{+, 0, 0}:0 + 0 =_\mathbb{Z} 0 from the rules for addition. For the case with the equivalence s:s:\mathbb{Z} \simeq \mathbb{Z}, the application to ss is itself a dependent function of a family of equivalences,

ap s: y: x:(y= x)(s(y)= s(x))\mathrm{ap}_{s}:\prod_{y:\mathbb{Z}} \prod_{x:\mathbb{Z}} (y =_\mathbb{Z} x) \simeq (s(y) =_\mathbb{Z} s(x))

Substituting 0+x0 + x and x+0x + 0 in for yy yields the family of equivalences

x:ap s(0+x,x):(0+x= x)(s(0+x)= s(x))x:\mathbb{Z} \vdash \mathrm{ap}_{s}(0 + x, x):(0 + x =_\mathbb{Z} x) \simeq (s(0 + x) =_\mathbb{Z} s(x))
x:ap s(x+0,x):(x+0= x)(s(x+0)= s(x))x:\mathbb{Z} \vdash \mathrm{ap}_{s}(x + 0, x):(x + 0 =_\mathbb{Z} x) \simeq (s(x + 0) =_\mathbb{Z} s(x))

and by the introduction rule of dependent product types, one gets the dependent functions of families of equivalences

λx:.ap s(0+x,x): x:(0+x= x)(s(0+x)= s(x))\lambda x:\mathbb{Z}.\mathrm{ap}_{s}(0 + x, x):\prod_{x:\mathbb{Z}} (0 + x =_\mathbb{Z} x) \simeq (s(0 + x) =_\mathbb{Z} s(x))
λx:.ap s(x+0,x): x:(x+0= x)(s(x+0)= s(x))\lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + 0, x):\prod_{x:\mathbb{Z}} (x + 0 =_\mathbb{Z} x) \simeq (s(x + 0) =_\mathbb{Z} s(x))

and by the elimination rules for the integers type, one has families of identifications

x:ind 0+x= x(β +,0,0,λx:.ap s(0+x,x),x):0+x= xx:\mathbb{Z} \vdash \mathrm{ind}_\mathbb{Z}^{0 + x =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(0 + x, x), x):0 + x =_\mathbb{Z} x
x:ind x+0= x(β +,0,0,λx:.ap s(x+0,x),x):x+0= xx:\mathbb{Z} \vdash \mathrm{ind}_\mathbb{Z}^{x + 0 =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + 0, x), x):x + 0 =_\mathbb{Z} x

By the introduction rule of dependent product types, one gets homotopies

λx:.ind 0+x= x(β +,0,0,λx:.ap s(0+x,x),x): x:0+x= x\lambda x:\mathbb{Z}.\mathrm{ind}_\mathbb{Z}^{0 + x =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(0 + x, x), x):\prod_{x:\mathbb{Z}} 0 + x =_\mathbb{Z} x
λx:.ind x+0= x(β +,0,0,λx:.ap s(x+0,x),x): x:x+0= x\lambda x:\mathbb{Z}.\mathrm{ind}_\mathbb{Z}^{x + 0 =_\mathbb{Z} x}(\beta_\mathbb{Z}^{+, 0, 0}, \lambda x:\mathbb{Z}.\mathrm{ap}_{s}(x + 0, x), x):\prod_{x:\mathbb{Z}} x + 0 =_\mathbb{Z} x

Thus, the integers type is a non-coherent H-space.

Theorem

The integers type is a non-coherent A3-space, an associative non-coherent H-space.

Proof

To do: figure out a way to prove that the integers type is 0-truncated without using the natural numbers type. Then we define the natural numbers type \mathbb{N} as the quotient of the integers type by its group of units / ×\mathbb{Z}/\mathbb{Z}^\times.

Theorem

The natural numbers type \mathbb{N} is 0-truncated.

Proof

Theorem

The natural numbers type \mathbb{N} and the integers type \mathbb{Z} are equivalent to each other.

Proof

Theorem

The integers type \mathbb{Z} is a monoid, a 0-truncated non-coherent A3-space.

Proof

Since \mathbb{N} is 0-truncated, and equivalences preserve truncatedness, by the equivalence e:e:\mathbb{N} \simeq \mathbb{Z}, \mathbb{Z} is also 0-truncated. Since \mathbb{Z} is a non-coherent A3-space, this implies that \mathbb{Z} is a monoid.

Theorem

The integers type is a group, a monoid such that given an integer x:x:\mathbb{Z}, left addition and right addition by xx is each an equivalence of types.

Proof

Theorem

The integers type is an abelian group.

Proof

Definition

The unary operation negation is defined by induction on the integers type

Introduction rules for negation:

ΓctxΓ,x:x:\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash -x:\mathbb{Z}}

Computation rules for negation:

ΓctxΓβ ,0:0= 0\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{-, 0}:-0 =_\mathbb{Z} 0}
ΓctxΓ,x:β ,s(x):s(x)= s 1(x)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{-, s}(x):-s(x) =_\mathbb{Z} s^{-1}(-x)}

where s 1:s^{-1}:\mathbb{Z} \simeq \mathbb{Z} is the inverse equivalence of s:s:\mathbb{Z} \simeq \mathbb{Z}.

Definition

The binary operation subtraction is defined as

xyx+(y)x - y \coloneqq x + (- y)

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Commutative ring structure on the integers

Definition

The integer number one 1:1:\mathbb{Z} is defined as

1s(0)1 \coloneqq s(0)
Definition

The binary operation multiplication is defined by double induction on the integers

Introduction rules for multiplication:

ΓctxΓ,x:,y:xy:\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash x \cdot y:\mathbb{Z}}

Computation rules for multiplication:

ΓctxΓβ ,0,0:00= 0\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{\cdot, 0, 0}:0 \cdot 0 =_\mathbb{Z} 0}
ΓctxΓ,x:β ,0,s(x):0s(x)= 0x+0\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\cdot, 0, s}(x):0 \cdot s(x) =_\mathbb{Z} 0 \cdot x + 0}
ΓctxΓ,x:β ,s,0(x):s(x)0= x0+0\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\cdot, s, 0}(x):s(x) \cdot 0 =_\mathbb{Z} x \cdot 0 + 0}
ΓctxΓ,x:,y:β ,s,s(x,y):s(x)s(y)= s(xy+x+y)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\cdot, s, s}(x, y):s(x) \cdot s(y) =_\mathbb{Z} s(x \cdot y + x + y)}
Definition

The binary operation exponentiation is defined by induction on the natural numbers

Introduction rules for exponentiation:

ΓctxΓ,n:,x:,x n:\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N}, x:\mathbb{Z}, \vdash x^n:\mathbb{Z}}

Computation rules for exponentiation:

ΓctxΓ,x:,β x (),0(x):x 0= 1\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, \vdash \beta_\mathbb{Z}^{x^{(-)}, 0}(x):x^0 =_\mathbb{Z} 1}
ΓctxΓ,n:,x:,β x (),s:x s(n)= x nx\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N}, x:\mathbb{Z}, \vdash \beta_\mathbb{Z}^{x^{(-)}, s}:x^{s(n)} =_\mathbb{Z} x^n \cdot x}
Definition

The inclusion of the natural numbers in the integers is inductively defined by induction on the natural numbers

Introduction rules for natural number inclusion:

ΓctxΓ,n:i(n):\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash i(n):\mathbb{Z}}

Computation rules for natural number inclusion:

ΓctxΓβ i,0:i(0)= 0\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{i, 0}:i(0) =_\mathbb{Z} 0}
ΓctxΓ,n:β i,s(n):i(s(n))= s(i(n))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \beta_\mathbb{Z}^{i, s}(n):i(s(n)) =_\mathbb{Z} s(i(n))}

Decidability of equality

Perhaps it is time to prove that equality is decidable on the integers.

Definition

The observational equality relation is defined by double induction on the integers

Formation rules for observational equality:

ΓctxΓ,x:,y:Eq (x,y)type\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \mathrm{Eq}_\mathbb{Z}(x, y) \; \mathrm{type}}

Definition rules for observational equality:

ΓctxΓβ Eq ,0,0:Eq (0,0)𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, 0}:\mathrm{Eq}_\mathbb{Z}(0, 0) \simeq \mathbb{1}}
ΓctxΓ,x:β Eq ,0,s:Eq (0,s(x))Eq (s 1(0),x)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, s}:\mathrm{Eq}_\mathbb{Z}(0, s(x)) \simeq \mathrm{Eq}_\mathbb{Z}(s^{-1}(0), x)}
ΓctxΓ,x:β Eq ,0,s:Eq (s(x),0)Eq (x,s 1(0))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, s}:\mathrm{Eq}_\mathbb{Z}(s(x), 0) \simeq \mathrm{Eq}_\mathbb{Z}(x, s^{-1}(0))}
ΓctxΓ,x:,y:β Eq ,s,s:Eq (s(x),s(y))Eq (x,y)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathbb{Z}, y:\mathbb{Z} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, s, s}:\mathrm{Eq}_\mathbb{Z}(s(x), s(y)) \simeq \mathrm{Eq}_\mathbb{Z}(x, y)}

The following rules only hold if the universe has a univalent universe:

ΓctxΓ,N:β Eq ,s,0:Eq (0,i(n)+1)𝟘\frac{\Gamma \; \mathrm{ctx}}{\Gamma, N:\mathbb{N} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, s, 0}:\mathrm{Eq}_\mathbb{Z}(0, i(n) + 1) \simeq \mathbb{0}}
ΓctxΓ,N:β Eq ,0,s:Eq (i(n)+1,0)𝟘\frac{\Gamma \; \mathrm{ctx}}{\Gamma, N:\mathbb{N} \vdash \beta_\mathbb{Z}^{\mathrm{Eq}_\mathbb{Z}, 0, s}:\mathrm{Eq}_\mathbb{Z}(i(n) + 1, 0) \simeq \mathbb{0}}

Order structure on the integers

Given a type family x:AB(x)x:A \vdash B(x), we define the existential quantifier x:A.B(x)\exists x:A.B(x) as the propositional truncation of the dependent sum type [ x:AB(x)]\left[\sum_{x:A} B(x)\right]. Given two types AA and BB, we define the disjunction ABA \vee B as the propositional truncation of the sum type [A+B]\left[A + B\right].

Definition

The predicate is less than, denoted as x<yx \lt y, is defined as

x<yn:.x+i(n)+1= yx \lt y \coloneqq \exists n:\mathbb{N}.x + i(n) + 1 =_\mathbb{N} y

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The predicate is greater than, denoted as x>yx \gt y, is defined as

x>yn:.x= y+i(n)+1x \gt y \coloneqq \exists n:\mathbb{N}.x =_\mathbb{N} y + i(n) + 1

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The predicate is apart from, denoted as x#yx # y, is defined as

x#y(x<y)(x>y)x # y \coloneqq (x \lt y) \vee (x \gt y)

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The predicate is less than or equal to, denoted as xyx \leq y, is defined as

xyn:.x+i(n)= yx \leq y \coloneqq \exists n:\mathbb{N}.x + i(n) =_\mathbb{N} y

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The predicate is greater than or equal to, denoted as xyx \geq y, is defined as

xyn:.x= y+i(n)x \geq y \coloneqq \exists n:\mathbb{N}.x =_\mathbb{N} y + i(n)

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The predicate is positive, denoted as isPositive(x)\mathrm{isPositive}(x), is defined as

isPositive(x)n:.i(n)+1= x\mathrm{isPositive}(x) \coloneqq \exists n:\mathbb{N}.i(n) + 1 =_\mathbb{N} x

for x:x:\mathbb{Z}.

Definition

The predicate is negative, denoted as isNegative(x)\mathrm{isNegative}(x), is defined as

isNegative(x)n:.x+i(n)+1= 0\mathrm{isNegative}(x) \coloneqq \exists n:\mathbb{N}.x + i(n) + 1 =_\mathbb{N} 0

for x:x:\mathbb{Z}.

Definition

The predicate is zero, denoted as isZero(x)\mathrm{isZero}(x), is defined as

isZero(x)x= 0\mathrm{isZero}(x) \coloneqq x =_\mathbb{Z} 0

for x:x:\mathbb{Z}.

Definition

The predicate is non-positive, denoted as isNonPositive(x)\mathrm{isNonPositive}(x), is defined as

isNonPositive(x)n:.0= x+i(n)\mathrm{isNonPositive}(x) \coloneqq \exists n:\mathbb{N}.0 =_\mathbb{N} x + i(n)

for x:x:\mathbb{Z}.

Definition

The predicate is non-negative, denoted as isNonNegative(x)\mathrm{isNonNegative}(x), is defined as

isNonNegative(x)n:.x= i(n)\mathrm{isNonNegative}(x) \coloneqq \exists n:\mathbb{N}.x =_\mathbb{N} i(n)

for x:x:\mathbb{Z}.

Definition

The predicate is non-zero, denoted as isNonZero(x)\mathrm{isNonZero}(x), is defined as

isNonZero(x)isPositive(x)isNegative(x)\mathrm{isNonZero}(x) \coloneqq \mathrm{isPositive}(x) \vee \mathrm{isNegative}(x)

for x:x:\mathbb{Z}.

Pseudolattice and metric structure on the integers

Definition

The ramp function ramp:\mathrm{ramp}:\mathbb{Z} \to \mathbb{Z} is defined as

ramp(i(n))i(n)\mathrm{ramp}(i(n)) \coloneqq i(n)
ramp((i(n)+1))0\mathrm{ramp}(-(i(n) + 1)) \coloneqq 0

for n:n:\mathbb{N}.

Definition

The minimum min:×\min:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

min(x,y)xramp(xy)\min(x,y) \coloneqq x - \mathrm{ramp}(x - y)

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The maximum max:×\max:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

max(x,y)x+ramp(yx)\max(x,y) \coloneqq x + \mathrm{ramp}(y - x)

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The metric ρ:×\rho:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z} is defined as

ρ(x,y)max(x,y)min(x,y)\rho(x,y) \coloneqq \max(x,y) - \min(x,y)

for x:x:\mathbb{Z}, y:y:\mathbb{Z}.

Definition

The absolute value |()|:\vert(-)\vert:\mathbb{Z} \to \mathbb{Z} is defined as

|x|max(x,x)\vert x \vert \coloneqq \max(x, -x)

for x:x:\mathbb{Z}.

Division and remainder

Definition

Integer division ()÷():× 0(-)\div(-):\mathbb{Z} \times \mathbb{Z}_{\neq 0} \to \mathbb{Z} is defined as

i(n)÷i(m)i(n÷m)i(n) \div i(m) \coloneqq i(n \div m)
i(n)÷i(m)i(n÷m)i(n) \div -i(m) \coloneqq -i(n \div m)
i(n)÷i(m)i(n÷m)-i(n) \div i(m) \coloneqq -i(n \div m)
i(n)÷i(m)i(n÷m)-i(n) \div -i(m) \coloneqq i(n \div m)

for n:n:\mathbb{N}, m: 0m:\mathbb{N}_{\neq 0}.

See also

References

For definitions as a higher inductive type in homotopy type theory, see:

A few more definitions of the integers, as well as the statement of the dependent universal property of the integers, could be found in:

Some terms about specific kinds of H-spaces used to prove properties of the integers are defined in:

A formalization in terms of homotopy type theory, using a unary notation, is in

(A different common formalization of integers in type theory is in a binary notation, as in the Coq standard library. Binary notation is exponentially more efficient for performing computations, but the unary notation was convenient for calculating π 1(S 1)\pi_1(S^1).)

Last revised on January 24, 2023 at 17:32:32. See the history of this page for a list of all contributions to it.