Contents
Idea
The integers as familiar from school mathematics.
Definitions
The type of integers, denoted , has several definitions as a higher inductive type.
Definition 1
The integers are defined as the higher inductive type generated by:
- A function .
- An identity representing that positive and negative zero are equal: .
Definition 2
The integers are defined as the higher inductive type generated by:
- A term .
- A function .
- A function .
- A function .
- A dependent product of identities representing that is a section of :
- A dependent product of identities representing that is a retracion of :
Definition 3
The integers are defined as the higher inductive type generated by:
- A term .
- A function .
- A function .
- A dependent product of identities representing that is a section of :
- A dependent product of identities representing that is a retracion of :
- A dependent product of identities representing the coherence condition:
Definition 4
The integers are defined as the higher inductive type generated by:
- A term .
- A function .
- A function .
- An identity representing that zero and negative zero are equal: .
- A dependent product of identities representing that negation is an involution:
- A dependent product of identities representing the coherence condition for the above:
- A dependent product of identities representing that is a section of :
- A dependent product of identities representing that is a retracion of :
- A dependent product of identities representing the coherence condition:
Definition 5
The integers are 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
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 is defined as
Definition
The binary operation addition is inductively defined as
for , , , .
Definition
The unary operation negation is defined as
for , ,
Definition
The binary operation subtraction is defined as
for , , , .
Definition
The integer number one is defined as
Definition
The binary operation multiplication is defined as
for , , , , , (exclusive or binary operation in ).
Definition
The right -action exponentiation is inductively defined as
for , , , .
Definition
The dependent type is positive, denoted as , is defined as
for , , dependent types indexed by .
Definition
The dependent type is negative, denoted as , is defined as
for , , dependent types indexed by .
Definition
The dependent type is zero, denoted as , is defined as
for , .
Definition
The dependent type is non-positive, denoted as is defined as
for , .
Definition
The dependent type is non-negative, denoted as , is defined as
for , .
Definition
The dependent type is non-zero, denoted as , is defined as
for , .
Definition
The dependent type is less than, denoted as , is defined as
for , , , .
Definition
The dependent type is greater than, denoted as , is defined as
for , , , .
Definition
The dependent type is apart from, denoted as , is defined as
for , , , .
Definition
The dependent type is less than or equal to, denoted as , is defined as
for , , , .
Definition
The dependent type is greater than or equal to, denoted as , is defined as
for , , , .
Definition
The ramp function is inductively defined as
for .
Definition
The minimum is defined as
for , , , .
Definition
The maximum is defined as
for , , , .
Definition
The absolute value is defined as
for , .
See also
References