Contents
Context
Type theory
Deduction and Induction
Foundations
foundations
The basis of it all
-
mathematical logic
-
deduction system, natural deduction, sequent calculus, lambda-calculus, judgment
-
type theory, simple type theory, dependent type theory
-
collection, object, type, term, set, element
-
equality, judgmental equality, typal equality
-
universe, size issues
-
higher-order logic
Set theory
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:
Introduction rules for the integers type:
Elimination rules for the integers type:
Computation rules for the integers type:
- Judgmental computation rules
Uniqueness rules for the integers type:
- Judgmental uniqueness rules
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:
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
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 :
As a quotient of a product type
Definition
The integers type is defined as the higher inductive type generated by:
- A function .
- An identity representing that positive and negative zero are equal: .
Definition
The integers type is defined as the higher inductive type generated by:
- A function .
- A dependent product of functions between identities representing that equivalent differences are equal:
- A set-truncator
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:
Computation rules for addition:
Theorem
The integers type is a non-coherent H-space with respect to the zero integer found in the introduction rule of the integers type and addition 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 , one gets the identity from the rules for addition. For the case with the equivalence , the application to is itself a dependent function of a family of equivalences,
Substituting and in for yields the family of equivalences
and by the introduction rule of dependent product types, one gets the dependent functions of families of equivalences
and by the elimination rules for the integers type, one has families of identifications
By the introduction rule of dependent product types, one gets homotopies
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.
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 as the quotient of the integers type by its group of units .
Theorem
The natural numbers type and the integers type are equivalent to each other.
Theorem
The integers type is a monoid, a 0-truncated non-coherent A3-space.
Proof
Since is 0-truncated, and equivalences preserve truncatedness, by the equivalence , is also 0-truncated. Since is a non-coherent A3-space, this implies that is a monoid.
Theorem
The integers type is a group, a monoid such that given an integer , left addition and right addition by is each an equivalence of types.
Theorem
The integers type is an abelian group.
Definition
The unary operation negation is defined by induction on the integers type
Introduction rules for negation:
Computation rules for negation:
where is the inverse equivalence of .
Definition
The binary operation subtraction is defined as
for , .
Commutative ring structure on the integers
Definition
The integer number one is defined as
Definition
The binary operation multiplication is defined by double induction on the integers
Introduction rules for multiplication:
Computation rules for multiplication:
Definition
The binary operation exponentiation is defined by induction on the natural numbers
Introduction rules for exponentiation:
Computation rules for exponentiation:
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:
Computation rules for natural number inclusion:
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:
Definition rules for observational equality:
The following rules only hold if the universe has a univalent universe:
Order structure on the integers
Given a type family , we define the existential quantifier as the propositional truncation of the dependent sum type . Given two types and , we define the disjunction as the propositional truncation of the sum type .
Definition
The predicate is less than, denoted as , is defined as
for , .
Definition
The predicate is greater than, denoted as , is defined as
for , .
Definition
The predicate is apart from, denoted as , is defined as
for , .
Definition
The predicate is less than or equal to, denoted as , is defined as
for , .
Definition
The predicate is greater than or equal to, denoted as , is defined as
for , .
Definition
The predicate is positive, denoted as , is defined as
for .
Definition
The predicate is negative, denoted as , is defined as
for .
Definition
The predicate is zero, denoted as , is defined as
for .
Definition
The predicate is non-positive, denoted as , is defined as
for .
Definition
The predicate is non-negative, denoted as , is defined as
for .
Definition
The predicate is non-zero, denoted as , is defined as
for .
Pseudolattice and metric structure on the integers
Definition
The ramp function is defined as
for .
Definition
The minimum is defined as
for , .
Definition
The maximum is defined as
for , .
Definition
The metric is defined as
for , .
Definition
The absolute value is defined as
for .
Division and remainder
Definition
Integer division is defined as
for , .
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 .)