module Data.Int.HIT where

# The integers as a HITπ

One of the possible characterisations of the integers is as the group
freely generated by the *monoid* of natural numbers under
addition. This module constructs this as a higher inductive type:

data Int : Type where diff : (x y : Nat) β Int quot : (m n : Nat) β diff m n β‘ diff (suc m) (suc n)

While this higher-inductive type is a perfectly workable definition
of the integers *from a mathematical point of view*, the
ergonomics of higher inductive types are still an area of active
research. Therefore, we prefer a βboringβ inductive representation of the
integers.

This is an alternative representation of the construction of the group integers as consisting of pairs $(x,y):N_{2},$ where $(a,b)$ is set identical to $(c,d)$ when $a+d=b+c.$ The single generating path $(a,b)βΌ(1+a,1+b)$ can be stretched to obtain this more familiar quotient, but it has the benefit of provably resulting in a set (without truncation). Intuitively, this is because we only identify points that βused to be distinctβ.

We can start by proving that all representations of zero are the same:

zeroes : (n : Nat) β diff 0 0 β‘ diff n n zeroes zero = refl zeroes (suc n) = zeroes n β quot _ _

Additionally, offsetting a difference by a fixed natural, as long as itβs done on both sides of the difference, does not change which integer is being represented: That is, considering all three naturals as integers, $(aβb)=(n+a)β(n+b).$

cancel : (a b n : Nat) β diff a b β‘ diff (n + a) (n + b) cancel a b zero = refl cancel a b (suc n) = cancel a b n β quot _ _

As a final pair of helper lemmas, we find that if $n$ and $k$ differ by an absolute value of $b,$ then the values $nβk$ and $b$ are the same (as long as we fix the sign β hence the two lemmas). The generic situation of βdiffering by $b$β is captured by fixing a natural number $a$ and adding $b,$ because we have $(a+b)βa=b$ and $aβ(a+b)=βb.$

offset-negative : (a b : Nat) β diff a (a + b) β‘ diff 0 b offset-negative zero b = refl offset-negative (suc a) b = diff (suc a) (suc (a + b)) β‘β¨ sym (quot _ _) β©β‘ diff a (a + b) β‘β¨ offset-negative a b β©β‘ diff 0 b β offset-positive : (a b : Nat) β diff (a + b) a β‘ diff b 0 offset-positive zero b = refl offset-positive (suc a) b = diff (suc (a + b)) (suc a) β‘β¨ sym (quot _ _) β©β‘ diff (a + b) a β‘β¨ offset-positive a b β©β‘ diff b 0 β

Those two are the last two lemmas we need to prove the βifβ direction
of βnaturals are identified in the quotient iff they represent the same
differenceβ: the construction `same-difference`

below packages
everything together with a bow on the top.

opaque same-difference : {a b c d : Nat} β a + d β‘ b + c β diff a b β‘ diff c d same-difference {zero} {b} {c} {d} path = sym $ diff c β d β β‘β¨ ap! path β©β‘ diff c β b + c β β‘β¨ ap! (+-commutative b c) β©β‘ diff c (c + b) β‘β¨ offset-negative _ _ β©β‘ diff 0 b β same-difference {suc a} {zero} {c} {d} path = sym $ diff β c β d β‘β¨ ap! (sym path) β©β‘ diff β suc a + d β d β‘β¨ ap! (+-commutative (suc a) d) β©β‘ diff (d + suc a) d β‘β¨ offset-positive _ _ β©β‘ diff (suc a) 0 β same-difference {suc a} {suc b} {c} {d} path = diff (suc a) (suc b) β‘Λβ¨ quot _ _ β©β‘Λ diff a b β‘β¨ same-difference (suc-inj path) β©β‘ diff c d β

quot-diamond : (a b : Nat) β Square (quot a b) (quot a b) (quot (suc a) (suc b)) (quot (suc a) (suc b)) quot-diamond a b i j = hcomp (β i β¨ β j) Ξ» where k (i = i0) β quot a b j k (i = i1) β quot (suc a) (suc b) (j β§ k) k (j = i0) β quot a b i k (j = i1) β quot (suc a) (suc b) (i β§ k) k (k = i0) β quot a b (i β¨ j) quot-triangle : (a b : Nat) (i : I) β diff a b β‘ quot a b i quot-triangle a b i j = hcomp (β j β¨ ~ i) Ξ» where k (i = i0) β diff a b k (j = i0) β diff a b k (k = i0) β diff a b k (j = i1) β quot a b (i β§ k)

In the other direction, we must be clever: we use path induction,
defining a type family
$Code_{a,b}(x)$
such that the fibre of
$Code_{a,b}$
over
$(c,d)$
is
$a+d=b+c.$
We can then use path induction to construct the map inverse to `same-difference`

. On the way,
the first thing we establish is a pair of observations about equalities
on the natural numbers:
$a+n=b+m$
and
$a+1+n=b+1+m$
are equivalent conditions. This can be seen by commutativity and
injectivity of the successor function, but below we prove it using
equational reasoning, without appealing to commutativity.

module β€-Path where private variable a b m n c d : Nat encode-p-from : (a + n β‘ b + m) β (a + suc n β‘ b + suc m) encode-p-from {a = a} {n} {b} {m} p = a + suc n β‘β¨ +-sucr a n β©β‘ suc (a + n) β‘β¨ ap suc p β©β‘ suc (b + m) β‘Λβ¨ +-sucr b m β©β‘Λ b + suc m β encode-p-to : (a + suc n β‘ b + suc m) β (a + n β‘ b + m) encode-p-to {a} {n} {b} {m} p = suc-inj (sym (+-sucr a n) β p β +-sucr b m)

We then define, fixing two natural numbers
$a,b,$
the family
$Code_{a,b}(x)$
by recursion on the integer
$x.$
Recall that we want the fibre over
$diff(c,d)$
to be
$a+d=b+c,$
so thatβs our pick. Now, the `quot`

path
constructor mandates that the fibre over
$(c,d)$
be the same as that over
$(1+c,1+d)$
β but this follows by propositional extensionality and the pair of
observations above.

Code : β (a b : Nat) (x : Int) β Type Code a b (diff c d) = a + d β‘ b + c Code a b (quot m n i) = path i where path : (a + n β‘ b + m) β‘ (a + suc n β‘ b + suc m) path = ua (prop-ext (Nat-is-set _ _) (Nat-is-set _ _) encode-p-from encode-p-to)

Hence, if we have a path
$diff(a,b)=x,$
we can apply path induction, whence it suffices to consider the case
where
$x$
is literally_ the difference of
$a$
and
$b.$
To lift this into our `Code`

fibration, we must show
that
$a+b=b+a,$
but this is exactly commutativity of addition on
$N.$

encode : β (a b : Nat) (x : Int) β diff a b β‘ x β Code a b x encode a b x = J (Ξ» x p β Code a b x) (+-commutative a b)

As a finishing touch, we give `Int`

instances for `Number`

and `Negative`

, meaning that we can use
positive and negative integer literals to denote values of `Int`

.

instance Number-Int : Number Int Number-Int .Number.Constraint _ = β€ Number-Int .Number.fromNat n = diff n 0 Negative-Int : Negative Int Negative-Int .Negative.Constraint _ = β€ Negative-Int .Negative.fromNeg n = diff 0 n

## Canonical representativesπ

Initially, we note that the type of integers admits a surjection from
the type
$NβN,$
given by sending each pair of naturals to their `difference`

.

private difference-surjection : β x β β (Nat Γ Nat) (Ξ» (a , b) β (diff a b β‘ x)) difference-surjection (diff x y) = inc ((x , y) , refl) difference-surjection (quot m n i) = is-propβpathp (Ξ» i β β₯_β₯.squash {A = Ξ£[ (a , b) β Nat Γ Nat ] (diff a b β‘ quot m n i)}) (inc ((m , n) , refl)) (inc ((suc m , suc n) , refl)) i

What weβll show is that this surjection actually *splits*:
Given an integer, we can find out what natural numbers it came from.
Well, not quite: We can find a reduced representation of that
difference. Namely, suppose weβre given the integer
$aβb.$
We split by cases:

- If $a<b,$ then this is the same integer as $0β(bβa);$
- If $a>b,$ then this is the same integer as $(aβb)β0;$
- If $a=b,$ then this is the same integer as $0β0.$

A βcanonical formβ for an integer is a pair of natural numbers that
represent (under `diff`

) the same
integer we started with. The canonicalisation procedure does the split
we described above, appealing to a battery of three lemmas to prove the
equality.

Canonical : Int β Type Canonical n = Ξ£[ x β Nat ] Ξ£[ y β Nat ] (diff x y β‘ n) canonicalise : (n : Int) β Canonical n canonicalise = go where lemmaβ : β x y β .(x < y) β diff 0 (y - x) β‘ diff x y lemmaβ : β x y β .(y < x) β diff (x - y) 0 β‘ diff x y lemmaβ : β x y β .(x β‘ y) β diff 0 0 β‘ diff x y work : β x y β Canonical (diff x y) work x y with β€-split x y ... | inl p = 0 , y - x , lemmaβ x y p ... | inr (inl p) = x - y , 0 , lemmaβ x y p ... | inr (inr p) = 0 , 0 , lemmaβ x y p

It remains to show that the procedure `work`

respects the quotient.
This is a truly gargantuan amount of work, and so itβs omitted from this
page. You can unfold it below if you dare:

## No, really, itβs quite ugly.

-- I commend your bravery in unfolding this <details>! These three -- lemmas are inductively defined on the natural numbers in a way that -- lets us prove that the paths they return respect the Int quotient -- without using that Int is a set (because we don't know that yet!) lemmaβ zero (suc y) p = refl lemmaβ (suc x) (suc y) p = lemmaβ x y (β€-peel p) β Int.quot x y lemmaβ (suc x) zero p = refl lemmaβ (suc x) (suc y) p = lemmaβ x y (β€-peel p) β Int.quot x y lemmaβ zero zero p = refl lemmaβ zero (suc y) p = absurd (zeroβ suc p) lemmaβ (suc x) zero p = absurd (sucβ zero p) lemmaβ (suc x) (suc y) p = lemmaβ x y (suc-inj p) β Int.quot x y abstract work-respects-quot : β x y β PathP (Ξ» i β Canonical (Int.quot x y i)) (work x y) (work (suc x) (suc y)) -- We split on (x, y) but also (1+x,1+y). This is obviously -- redundant to a human, but to Agda, we must do this: there is no -- link between these two splits. work-respects-quot x y with β€-split x y | β€-split (suc x) (suc y) ... | inl x<y | inl (sβ€s x<y') = Ξ£-pathp refl $ Ξ£-pathp refl $ commutesβsquare (β-idl _) ... | inr (inl x>y) | inr (inl (sβ€s x>y')) = Ξ£-pathp refl $ Ξ£-pathp refl $ commutesβsquare (β-idl _) ... | inr (inr xβ‘y) | inr (inr xβ‘y') = Ξ£-pathp refl $ Ξ£-pathp refl $ commutesβsquare (β-idl _) -- This *barrage* of cases is to handle the cases where e.g. (x < y) -- but (1 + x > 1 + y), which is "obviously" impossible. But Agda -- doesn't care about what humans think is obvious. ... | inl x<y | inr (inl (sβ€s x>y)) = absurd (<-asym x<y x>y) ... | inl x<y | inr (inr xβ‘y) = absurd (<-not-equal x<y (suc-inj xβ‘y)) ... | inr (inl x>y) | inl (sβ€s x<y) = absurd (<-asym x>y x<y) ... | inr (inr xβ‘y) | inl (sβ€s x<y) = absurd (<-not-equal x<y xβ‘y) ... | inr (inl x>y) | inr (inr xβ‘y) = absurd (<-not-equal x>y (sym (suc-inj xβ‘y))) ... | inr (inr xβ‘y) | inr (inl (sβ€s x>y)) = absurd (<-irrefl (sym xβ‘y) x>y) go : β n β Canonical n go (diff x y) = work x y go (Int.quot x y i) = work-respects-quot x y i

This *immediately* implies that the type of integers is a set,
because itβs a retract of a set β namely
$NΓN!$

instance abstract H-Level-Int : β {n} β H-Level Int (2 + n) H-Level-Int = basic-instance 2 (retractβis-hlevel 2 into from linv (hlevel 2)) where into : (Nat Γ Nat) β Int into (x , y) = diff x y from : Int β Nat Γ Nat from x with canonicalise x ... | a , b , p = a , b linv : β x β into (from x) β‘ x linv x with canonicalise x ... | a , b , p = p

# Recursionπ

If we want to define a map $f:ZβX,$ it suffices to give a function $f:N_{2}βX$ which respects the quotient, in the following sense:

Int-rec : β {β} {X : Type β} β (f : Nat β Nat β X) β (q : (a b : _) β f a b β‘ f (suc a) (suc b)) β Int β X Int-rec f q (diff x y) = f x y Int-rec f q (quot m n i) = q m n i

However, since
$X$
can be a more general space, not necessarily a *set*, defining a
*binary* operation
$f_{β²}:Z_{2}βX$
can be quite involved! It doesnβt suffice to exhibit a function from
$N_{4}$
which respects the quotient separately in each argument:

Int-recβ : β {β} {B : Type β} β (f : Nat Γ Nat β Nat Γ Nat β B) β (pl : (a b x y : _) β f (a , b) (x , y) β‘ f (suc a , suc b) (x , y)) β (pr : (a b x y : _) β f (a , b) (x , y) β‘ f (a , b) (suc x , suc y))

In addition, we must have that these two *paths*
`pl`

and `pr`

are *coherent*. There are two
ways of obtaining an equality
$f(a,b,x,y)=f(Sa,Sb,Sx,Sy)$
(`pl`

after `pr`

and `pr`

after
`pl`

, respectively) and these *must* be homotopic:

β (square : (a b x y : _) β Square (pl a b x y) (pr a b x y) (pr (suc a) (suc b) x y) (pl a b (suc x) (suc y))) β Int β Int β B

The type of `square`

says that we need the following
square of paths to commute, which says exactly that `pl β pr`

and `pr β pl`

are homotopic and imposes no further structure
on
$X$^{1}:

Int-recβ f p-l p-r sq (diff a b) (diff x y) = f (a , b) (x , y) Int-recβ f p-l p-r sq (diff a b) (quot x y i) = p-r a b x y i Int-recβ f p-l p-r sq (quot a b i) (diff x y) = p-l a b x y i Int-recβ f p-l p-r sq (quot a b i) (quot x y j) = sq a b x y i j

However, when the type
$X$
we are mapping into `is a set`

, as is the case for
the integers themselves, the square is automatically satisfied, so we
can give a simplified recursion principle:

Int-recβ-set : β {β} {B : Type β} β¦ iss-b : H-Level B 2 β¦ β (f : Nat Γ Nat β Nat Γ Nat β B) β (pl : (a b x y : _) β f (a , b) (x , y) β‘ f (suc a , suc b) (x , y)) β (pr : (a b x y : _) β f (a , b) (x , y) β‘ f (a , b) (suc x , suc y)) β Int β Int β B Int-recβ-set β¦ iss-b β¦ f pl pr = Int-recβ f pl pr square where abstract square : (a b x y : Nat) β PathP (Ξ» i β pl a b x y i β‘ pl a b (suc x) (suc y) i) (pr a b x y) (pr (suc a) (suc b) x y) square a b x y = is-setβsquarep (Ξ» i j β hlevel 2) _ _ _ _

Furthermore, when proving * propositions* of the
integers, the quotient is automatically respected, so it suffices to
give the case for

`diff`

:Int-elim-prop : β {β} {P : Int β Type β} β ((x : Int) β is-prop (P x)) β (f : (a b : Nat) β P (diff a b)) β (x : Int) β P x Int-elim-prop pprop f (diff a b) = f a b Int-elim-prop pprop f (quot m n i) = is-propβpathp (Ξ» i β pprop (quot m n i)) (f m n) (f (suc m) (suc n)) i

## There are also variants for binary and ternary predicates.

Int-elimβ-prop : β {β} {P : Int β Int β Type β} β ((x y : Int) β is-prop (P x y)) β (f : (a b x y : Nat) β P (diff a b) (diff x y)) β (x : Int) (y : Int) β P x y Int-elimβ-prop pprop f = Int-elim-prop (Ξ» x β Ξ -is-hlevel 1 (pprop x)) Ξ» a b int β Int-elim-prop (Ξ» x β pprop (diff a b) x) (f a b) int Int-elimβ-prop : β {β} {P : Int β Int β Int β Type β} β ((x y z : Int) β is-prop (P x y z)) β (f : (a b c d e f : Nat) β P (diff a b) (diff c d) (diff e f)) β (x : Int) (y : Int) (z : Int) β P x y z Int-elimβ-prop pprop f = Int-elimβ-prop (Ξ» x y β Ξ -is-hlevel 1 (pprop x y)) Ξ» a b c d int β Int-elim-prop (Ξ» x β pprop (diff a b) (diff c d) x) (f a b c d) int

A third possibility for elimination is granted to us by the
canonicalisation procedure: By canonicalising and looking at the
resulting minuend and subtrahend^{2}, we can split on an
integer based on its sign:

abstract canonicalise-not-both-suc : β x {k n} β canonicalise x .fst β‘ suc k β Β¬ canonicalise x .snd .fst β‘ suc n canonicalise-not-both-suc = Int-elim-prop {P = Ξ» x β β {k n} β canonicalise x .fst β‘ suc k β Β¬ canonicalise x .snd .fst β‘ suc n } (Ξ» p β hlevel 1) go where go : β a b {k n} β canonicalise (diff a b) .fst β‘ suc k β Β¬ canonicalise (diff a b) .snd .fst β‘ suc n go a b p q with β€-split a b ... | inl x = absurd (zeroβ suc p) ... | inr (inl x) = absurd (zeroβ suc q) ... | inr (inr x) = absurd (zeroβ suc q)

Int-elim-by-sign : β {β} (P : Int β Type β) β (pos : β x β P (diff x 0)) β (neg : β x β P (diff 0 x)) β P (diff 0 0) β β x β P x Int-elim-by-sign P pos neg zer x with inspect (canonicalise x) ... | (zero , zero , p) , q = subst P p zer ... | (zero , suc b , p) , q = subst P p (neg (suc b)) ... | (suc a , zero , p) , q = subst P p (pos (suc a)) ... | (suc a , suc b , p) , q = absurd (canonicalise-not-both-suc x (ap fst q) (ap (fst β snd) q))

data By-sign-view : Int β Type where posv : β z β By-sign-view (diff z 0) negv : β z β By-sign-view (diff 0 (suc z)) by-sign : β x β By-sign-view x by-sign = Int-elim-by-sign (Ξ» z β By-sign-view z) posv (Ξ» { zero β posv 0 ; (suc x) β negv x }) (posv 0)

This procedure is useful, for instance, for computing absolute values:

abs : Int β Nat abs x with by-sign x ... | posv z = z ... | negv z = suc z _ : abs -10 β‘ 10 _ = refl

# Algebraπ

With these recursion and elimination helpers, it becomes routine to lift the algebraic operations from naturals to integers:

## Successorsπ

The simplest βalgebraic operationβ on an integer is taking its successor. In fact, the integers are characterised by being the free type with an equivalence - that equivalence being βsuccessorβ.

sucβ€ : Int β Int sucβ€ (diff x y) = diff (suc x) y sucβ€ (quot m n i) = quot (suc m) n i predβ€ : Int β Int predβ€ (diff x y) = diff x (suc y) predβ€ (quot m n i) = quot m (suc n) i

The successor of
$(a,b)$
is
$(1+a,b).$
Similarly, the predecessor of
$(a,b)$
is
$(a,1+b).$
By the generating equality `quot`

, we have that
predecessor and successor are inverses, since applying both (in either
order) takes
$(a,b)$
to
$(1+a,1+b).$

pred-sucβ€ : (x : Int) β predβ€ (sucβ€ x) β‘ x pred-sucβ€ (diff x y) = sym (quot x y) pred-sucβ€ (quot m n i) j = quot-diamond m n i (~ j) suc-predβ€ : (x : Int) β sucβ€ (predβ€ x) β‘ x suc-predβ€ (diff x y) = sym (quot x y) suc-predβ€ (quot m n i) j = quot-diamond m n i (~ j) sucβ€-is-equiv : is-equiv sucβ€ sucβ€-is-equiv = is-isoβis-equiv (iso predβ€ suc-predβ€ pred-sucβ€) predβ€-is-equiv : is-equiv predβ€ predβ€-is-equiv = is-isoβis-equiv (iso sucβ€ pred-sucβ€ suc-predβ€)

## Additionπ

_+β€_ : Int β Int β Int diff a b +β€ diff c d = diff (a + c) (b + d) diff x y +β€ quot m n i = (quot (x + m) (y + n) β sym (apβ diff (+-sucr x m) (+-sucr y n))) i quot m n i +β€ diff x y = quot (m + x) (n + y) i quot m n i +β€ quot m' n' j = is-setβsquarep (Ξ» i j β hlevel 2) (Ξ» j β quot (m + m') (n + n') j) (quot (m + m') (n + n') β sym (apβ diff (+-sucr m m') (+-sucr n n'))) ( quot (suc (m + m')) (suc (n + n')) β sym (apβ diff (ap suc (+-sucr m m')) (ap suc (+-sucr n n')))) (Ξ» j β quot (m + suc m') (n + suc n') j) i j

Since addition of integers is (essentially!) addition of pairs of
naturals, the algebraic properties of `+`

on the natural
numbers automatically lift to properties about `_+β€_`

, using the
recursion helpers for props (`Int-elim-prop`

) and the fact
that equality of integers is a proposition.

+β€-associative : (x y z : Int) β x +β€ (y +β€ z) β‘ (x +β€ y) +β€ z +β€-zerol : (x : Int) β 0 +β€ x β‘ x +β€-zeror : (x : Int) β x +β€ 0 β‘ x +β€-commutative : (x y : Int) β x +β€ y β‘ y +β€ x

## See the proofs here

abstract +β€-associative = Int-elimβ-prop (Ξ» x y z β hlevel 1) (Ξ» a b c d e f β apβ diff (+-associative a c e) (+-associative b d f)) +β€-zerol = Int-elim-prop (Ξ» x β hlevel 1) (Ξ» a b β refl) +β€-zeror = Int-elim-prop (Ξ» x β hlevel 1) (Ξ» a b β apβ diff (+-zeror a) (+-zeror b)) +β€-commutative = Int-elimβ-prop (Ξ» x y β hlevel 1) (Ξ» a b c d β apβ diff (+-commutative a c) (+-commutative b d))

## Inversesπ

Every integer
$x$
has an additive inverse, denoted
$βx,$
which is obtained by swapping the components of the pair. Since the
definition of `negate`

is very simple, it can
be written conveniently without using `Int-rec`

:

negate : Int β Int negate (diff x y) = diff y x negate (quot m n i) = quot n m i

The proof that
$βx$
is an additive inverse to
$x$
follows, essentially, from commutativity of addition on natural numbers,
and the fact that `all zeroes are identified`

.

abstract +β€-inverser : (x : Int) β x +β€ negate x β‘ 0 +β€-inverser = Int-elim-prop (Ξ» _ β hlevel 1) Ξ» where a b β diff (a + b) β b + a β β‘β¨ ap! (+-commutative b a) β©β‘ diff (a + b) (a + b) β‘β¨ sym (zeroes (a + b)) β©β‘ diff 0 0 β +β€-inversel : (x : Int) β negate x +β€ x β‘ 0 +β€-inversel = Int-elim-prop (Ξ» _ β hlevel 1) Ξ» where a b β diff β b + a β (a + b) β‘β¨ ap! (+-commutative b a) β©β‘ diff (a + b) (a + b) β‘β¨ sym (zeroes (a + b)) β©β‘ diff 0 0 β

Since `negate`

is precisely whatβs
missing for `Nat`

to be a group, we
*can* turn the integers into a group. Subtraction is defined as
addition with the inverse, rather than directly on `diff`

:

_-β€_ : Int β Int β Int x -β€ y = x +β€ negate y

## Multiplicationπ

We now prove that the integers are a *ring*, i.e.Β that there
is a multiplication operation
$xβy$
with 1 as a left/right identity, which is associative, and additionally
distributes over addition on both the left and the right. Itβs also
commutative β so
$Z$
is a *commutative* ring.

The definition of multiplication is slightly tricky: We use the
binomial theorem. Pretend that
$xy$
is really
$(aβb)(cβd),$
and expand that to
$(ac+bd)β(ad+bc):$
thatβs our product. It remains to show that this respects the defining
equation `quot`

, which
involves some nasty equations (you can see them in the types of `lβ`

and `lβ`

below) β but this can be
done with the semiring solver.

module _ where private abstract lβ : β a b x y β a * x + b * y + (suc a * y + suc b * x) β‘ a * y + b * x + (suc a * x + suc b * y) lβ a b x y = nat! lβ : β a b x y β a * x + b * y + (a * suc y + b * suc x) β‘ a * y + b * x + (a * suc x + b * suc y) lβ a b x y = nat! rhsβ : β x y m n β diff (x * m + y * n) (x * n + y * m) β‘ diff (x * suc m + y * suc n) (x * suc n + y * suc m) rhsβ x y m n = same-difference (lβ x y m n) rhsβ : β x y m n β diff (m * x + n * y) (m * y + n * x) β‘ diff (x + m * x + (y + n * y)) (y + m * y + (x + n * x)) rhsβ x y m n = same-difference (lβ m n x y)

_*β€_ : Int β Int β Int diff a b *β€ diff c d = diff (a * c + b * d) (a * d + b * c) diff x y *β€ quot m n i = rhsβ x y m n i quot m n i *β€ diff x y = rhsβ x y m n i quot m n i *β€ quot x y j = is-setβsquarep (Ξ» i j β hlevel 2) (rhsβ x y m n) (rhsβ m n x y) (rhsβ (suc m) (suc n) x y) (rhsβ (suc x) (suc y) m n) i j

We omit the proofs of the arithmetic identities below since they are essentially induction + calling the semiring solver.

abstract *β€-associative : β x y z β x *β€ (y *β€ z) β‘ (x *β€ y) *β€ z *β€-commutative : β x y β x *β€ y β‘ y *β€ x *β€-idl : β x β 1 *β€ x β‘ x *β€-idr : β x β x *β€ 1 β‘ x *β€-distrib-+β€-l : β x y z β x *β€ (y +β€ z) β‘ (x *β€ y) +β€ (x *β€ z) *β€-distrib-+β€-r : β x y z β (y +β€ z) *β€ x β‘ (y *β€ x) +β€ (z *β€ x)

*β€-associative = Int-elimβ-prop (Ξ» _ _ _ β hlevel 1) Ξ» a b c d e f β sym (same-difference (lemma a b c d e f)) where abstract lemma : β a b c d e f β (a * c + b * d) * e + (a * d + b * c) * f + (a * (c * f + d * e) + b * (c * e + d * f)) β‘ (a * c + b * d) * f + (a * d + b * c) * e + (a * (c * e + d * f) + b * (c * f + d * e)) lemma a b c d e f = nat! *β€-commutative = Int-elimβ-prop (Ξ» _ _ β hlevel 1) Ξ» a b x y β same-difference (lemma a b x y) where abstract lemma : β a b x y β a * x + b * y + (x * b + y * a) β‘ a * y + b * x + (x * a + y * b) lemma a b x y = nat! *β€-idl = Int-elim-prop (Ξ» _ β hlevel 1) (Ξ» a b β same-difference (lemma a b)) where abstract lemma : β a b β (a + 0 + 0 + b) β‘ (b + 0 + 0 + a) lemma a b = nat! *β€-idr = Int-elim-prop (Ξ» _ β hlevel 1) (Ξ» a b β same-difference (lemma a b)) where abstract lemma : β a b β a * 1 + b * 0 + b β‘ a * 0 + b * 1 + a lemma a b = nat! *β€-distrib-+β€-l = Int-elimβ-prop (Ξ» _ _ _ β hlevel 1) Ξ» a b c d e f β same-difference (lemma a b c d e f) where abstract lemma : β a b c d e f β a * (c + e) + b * (d + f) + (a * d + b * c + (a * f + b * e)) β‘ a * (d + f) + b * (c + e) + (a * c + b * d + (a * e + b * f)) lemma a b c d e f = nat! *β€-distrib-+β€-r = Int-elimβ-prop (Ξ» _ _ _ β hlevel 1) Ξ» a b c d e f β same-difference (lemma a b c d e f) where lemma : β a b c d e f β (c + e) * a + (d + f) * b + (c * b + d * a + (e * b + f * a)) β‘ (c + e) * b + (d + f) * a + (c * a + d * b + (e * a + f * b)) lemma a b c d e f = nat! canonicalise-injective : β x y β canonicalise x .fst β‘ canonicalise y .fst β canonicalise x .snd .fst β‘ canonicalise y .snd .fst β x β‘ y canonicalise-injective = Int-elimβ-prop (Ξ» _ _ β hlevel 1) Ξ» a b x y p q β sym (canonicalise (diff a b) .snd .snd) Β·Β· apβ diff p q Β·Β· canonicalise (diff x y) .snd .snd instance Discrete-Int : Discrete Int Discrete-Int = go _ _ where goβ : (a b x y : Nat) β Dec (diff a b β‘ diff x y) goβ a b x y with a + y β‘? b + x ... | yes p = yes (same-difference p) ... | no Β¬p = no Ξ» ab β Β¬p (β€-Path.encode a b (diff x y) ab) goβ : (a b : Nat) (y : Int) β Dec (diff a b β‘ y) goβ a b (diff x y) = goβ a b x y goβ a b (quot m n i) = is-propβpathp (Ξ» i β Dec-is-hlevel 1 (hlevel {T = diff a b β‘ quot m n i} 1)) (goβ a b m n) (goβ a b (suc m) (suc n)) i go : β x y β Dec (x β‘ y) go (diff a b) y = goβ a b y go (quot m n i) y = is-propβpathp (Ξ» i β Dec-is-hlevel 1 (hlevel {T = quot m n i β‘ y} 1)) (goβ m n y) (goβ (suc m) (suc n) y) i

In the diagram, we write $Sx$ for

`suc x`

.β©οΈkeeping in mind that the image of

`canonicalise`

is restricted to pairs of the form $(0,1+x),$ $(1+x,0),$ or $(0,0)$β©οΈ