open import 1Lab.Prelude
open import 1Lab.Rewrite

open import Data.Nat.Solver
open import Data.Dec
open import Data.Nat
open import Data.Sum

module Data.Int where


# Integersπ

The integers are what you get when you complete the additive monoid structure on the naturals into a group. In non-cubical Agda, a representation of the integers as a coproduct $\mathbb{N} \coprod \mathbb{N}$ with one of the factors offset (to avoid having two zeroes) is adopted. In Cubical Agda we can adopt a representation much closer to a βclassicalβ construction of the integers:

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


This is an alternative representation of the construction of integers as pairs $(x , y)\colon \mathbb{N}^2$ where $(a,b) = (c, d)$ iff $a + d = b + c$: An integer is an equivalence class of pairs of naturals, where $(a, b)$ is identified with $(1 + a, 1 + b)$, or, more type-theoretically, the integers are generated by the constructor diff which embeds a pair of naturals, and the path constructor quot which expresses that $(a, b)$ = $(1 + a, 1 + b)$.

This single generating path is enough to recover the βclassicalβ quotient, which we do in steps. First, weβ¦ prove that that $n - n$ is $0$:

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 $\mathrm{Code}_{a,b}(x)$ such that the fibre of $\mathrm{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 $\mathrm{Code}_{a,b}(x)$ by recursion on the integer $x$. Recall that we want the fibre over $\mathrm{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 $\mathrm{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 $\mathbb{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 $\mathbb{N} \to \mathbb{N}$, given by sending each pair of naturals to their difference. private difference-surjection : β x β β[ (a , b) β Nat Γ Nat ] (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 $\mathbb{N} \times \mathbb{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 : \mathbb{Z} \to X$, it suffices to give a function $f : \mathbb{N}^2 \to 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' : \mathbb{Z}^2 \to X$ can be quite involved! It doesnβt suffice to exhibit a function from $\mathbb{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(\mathrm{S}a,\mathrm{S}b,\mathrm{S}x,\mathrm{S}y)$ (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

_ = is-set


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 subtrahend2, 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β€)


_+β€_ : 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 $\mathbb{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 inspect (a + y == b + x)
... | true , p  = yes (same-difference (is-equalβpath {a + y} {b + x} p))
... | false , p = no Ξ» q β is-not-equalβnot-path
{a + y} {b + x} p (β€-Path.encode a b (diff x y) q)

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


1. In the diagram, we write $\mathrm{S}x$ for suc x.β©οΈ

2. keeping in mind that the image of canonicalise is restricted to pairs of the form $(0,1+x)$, $(1+x,0)$, or $(0,0)$β©οΈ