Homotopy Type Theory integers > history (Rev #13)

Idea
Definitions
Properties
See also
References

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 : \mathbf{2} \times \mathbb{N} \rightarrow \mathbb{Z}$ .
An identity representing that positive and negative zero are equal: $\nu_0: inj(0, 0) = inj(1, 0)$ .

Definition 2

The integers are defined as the higher inductive type generated by:

A term $0 : \mathbb{Z}$ .
A function $s : \mathbb{Z} \to \mathbb{Z}$ .
A function $p_1 : \mathbb{Z} \to \mathbb{Z}$ .
A function $p_2 : \mathbb{Z} \to \mathbb{Z}$ .
A dependent product of identities representing that $p_1$ is a section of $s$ :
$\sigma: \prod_{a:\mathbb{Z}} p_1(s(a)) = a$
A dependent product of identities representing that $p_2$ is a retracion of $s$ :
$\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 : \mathbb{Z}$ .
A function $s : \mathbb{Z} \to \mathbb{Z}$ .
A function $p : \mathbb{Z} \to \mathbb{Z}$ .
A dependent product of identities representing that $p$ is a section of $s$ :
$\sigma: \prod_{a:\mathbb{Z}} p(s(a)) = a$
A dependent product of identities representing that $p$ is a retracion of $s$ :
$\rho: \prod_{a:\mathbb{Z}} s(p(a)) = a$
A dependent product of identities representing the coherence condition:
$\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 : \mathbb{Z}$ .
A function $s : \mathbb{Z} \to \mathbb{Z}$ .
A function $n : \mathbb{Z} \to \mathbb{Z}$ .
An identity representing that zero and negative zero are equal: $\nu: n(0) = 0$ .
A dependent product of identities representing that negation is an involution:
$\iota: \prod_{a:\mathbb{Z}} n(n(a)) = a$
A dependent product of identities representing the coherence condition for the above:
$\kappa_\iota: \prod_{a:\mathbb{Z}} ap_n(\iota(a)) = \iota(a)$
A dependent product of identities representing that $n \circ s \circ n$ is a section of $s$ :
$\sigma: \prod_{a:\mathbb{Z}} n(s(n(s(a)))) = a$
A dependent product of identities representing that $n \circ s \circ n$ is a retracion of $s$ :
$\rho: \prod_{a:\mathbb{Z}} s(n(s(n(a)))) = a$
A dependent product of identities representing the coherence condition:
$\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 : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{Z}$ .
A dependent product of functions between identities representing that equivalent differences are equal:
$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
$\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:\mathbb{Z}$ is defined as

0 \coloneqq inj(0, 0)

Definition

The binary operation addition $(-)+(-):\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ is inductively defined as

inj(0,a) + inj(0,b) \coloneqq inj(0,a+b)

inj(1,a) + inj(1,b) \coloneqq inj(1,a+b)

inj(0,0) + inj(1,a) \coloneqq inj(1,a)

inj(0,a) + inj(1,0) \coloneqq inj(0,a)

inj(0,s(a)) + inj(1,s(b)) \coloneqq inj(0,a) + inj(1,b)

inj(1,0) + inj(0,a) \coloneqq inj(0,a)

inj(1,a) + inj(0,0) \coloneqq inj(1,a)

inj(1,s(a)) + inj(0,s(b)) \coloneqq inj(1,a) + inj(0,b)

for $a:\mathbb{N}$ , $b:\mathbb{N}$ , $(-)+(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ , $s:\mathbb{N} \to \mathbb{N}$ .

Definition

The unary operation negation $-(-):\mathbb{Z} \to \mathbb{Z}$ is defined as

-inj(a, b) \coloneqq inj(\neg a, b)

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $\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) \coloneqq inj(a, b) + inj(\neg c, d)

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

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

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) \cdot inj(c,d) \coloneqq inj(a \oplus c,b \cdot d)

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ , $(-)\cdot(-):\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ , $(-)\oplus(-):\mathbf{2} \times \mathbf{2} \to \mathbf{2}$ (exclusive or binary operation in $\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 \coloneqq inj(0,1)

inj(a,b)^{2n} \coloneqq inj(0,b^{2n})

inj(a,b)^{2n+1} \coloneqq inj(a,b^{2n+1})

for $a:\mathbf{2}$ , $b:\mathbb{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))$ , is defined as

isPositive(inj(a,b)) \coloneqq (a = 0) \times (b \gt 0)

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , dependent types $m\gt n$ indexed by $m, n:\mathbb{N}$ .

Definition

The dependent type is negative, denoted as $isNegative(inj(a,b))$ , is defined as

isPositive(inj(a,b)) \coloneqq (a = 1) \times (b \gt 0)

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , dependent types $m\gt n$ indexed by $m, n:\mathbb{N}$ .

Definition

The dependent type is zero, denoted as $isZero(inj(a,b))$ , is defined as

isZero(inj(a,b)) \coloneqq b = 0

for $a:\mathbf{2}$ , $b:\mathbb{N}$ .

Definition

The dependent type is non-positive, denoted as $isNonPositive(inj(a,b))$ is defined as

isNonPositive(inj(a,b)) \coloneqq isPositive(inj(a,b)) \to \emptyset

for $a:\mathbf{2}$ , $b:\mathbb{N}$ .

Definition

The dependent type is non-negative, denoted as $isNonNegative(inj(a,b))$ , is defined as

isNonNegative(inj(a,b)) \coloneqq isNegative(inj(a,b)) \to \emptyset

for $a:\mathbf{2}$ , $b:\mathbb{N}$ .

Definition

The dependent type is non-zero, denoted as $isNonZero(inj(a,b))$ , is defined as

isNonZero(inj(a,b)) \coloneqq \Vert isPositive(inj(a,b)) + isNegative(inj(a,b)) \Vert

for $a:\mathbf{2}$ , $b:\mathbb{N}$ .

Definition

The dependent type is less than, denoted as $inj(a,b) \lt inj(c,d)$ , is defined as

$inj(a,b) \lt inj(c,d) \coloneqq isPositive(inj(c,d) - inj(a,b))$

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

The dependent type is greater than, denoted as $inj(a,b) \gt inj(c,d)$ , is defined as

$inj(a,b) \gt inj(c,d) \coloneqq isNegative(inj(c,d) - inj(a,b))$

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

The dependent type is apart from, denoted as $inj(a,b) # inj(c,d)$ , is defined as

$inj(a,b) # inj(c,d) \coloneqq isNonZero(inj(c,d) - inj(a,b))$

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

The dependent type is less than or equal to, denoted as $inj(a,b) \leq inj(c,d)$ , is defined as

$inj(a,b) \leq inj(c,d) \coloneqq isNonNegaitve(inj(c,d) - inj(a,b))$

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

The dependent type is greater than or equal to, denoted as $inj(a,b) \geq inj(c,d)$ , is defined as

$inj(a,b) \geq inj(c,d) \coloneqq isNonPositive(inj(c,d) - inj(a,b))$

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Pseudolattice structure on the integers

Definition

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

ramp(inj(0, a)) \coloneqq inj(0, a)

ramp(inj(1, a)) \coloneqq 0

for $a:\mathbb{N}$ .

Definition

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

min(inj(a,b),inj(c,d)) \coloneqq inj(a,b) - ramp(inj(a,b) - inj(c,d))

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

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

max(inj(a,b),inj(c,d)) \coloneqq inj(a,b) + ramp(inj(c,d) - inj(a,b))

for $a:\mathbf{2}$ , $b:\mathbb{N}$ , $c:\mathbf{2}$ , $d:\mathbb{N}$ .

Definition

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

\vert inj(a,b) \vert \coloneqq max(inj(a,b), -inj(a,b))

for $a:\mathbf{2}$ , $b:\mathbb{N}$ .

References

Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
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 April 14, 2022 at 15:41:56 by Anonymous?. See the history of this page for a list of all contributions to it.

Homotopy Type Theory integers > history (Rev #13)

Contents

Idea

Definitions

Definition 1

Definition 2

Definition 3

Definition 4

Definition 5

Properties

Commutative ring structure on the integers

Definition

Definition

Definition

Definition

Definition

Definition

Definition

Order structure on the integers

Definition

Definition

Definition

Definition

Definition

Definition

Definition

Definition

Definition

Definition

Definition

Pseudolattice structure on the integers

Definition

Definition

Definition

Definition

See also

References