open import 1Lab.Prelude open import Data.Nat.Solver 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
$\bb{N} \coprod \bb{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 \bb{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.

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 β

In the other direction, we must be clever: we use path induction, defining a type family $\id{Code}_{a,b}(x)$ such that the fibre of $\id{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 $\id{Code}_{a,b}(x)$ by recursion on the integer $x$. Recall that we want the fibre over $\id{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 $\id{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 $\bb{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
$\bb{N} \to \bb{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 p β Int.quot x y lemmaβ (suc x) zero p = refl lemmaβ (suc x) (suc y) p = lemmaβ x y 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 (zeroβ suc (sym 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. -- These first three cases basically mirror the definition of -- lemmaβ, lemmaβ, and lemmaβ. They show that -- lemmaβββ (suc x) (suc y) p β‘ lemmaβββ (suc x) (suc y) p' β Int.quot x y -- but mediating between SquareP, Β·Β·, and β. work-respects-quot x y with β€-split x y | β€-split (suc x) (suc y) ... | inl x<y | inl x<y' = Ξ£-pathp-dep refl $ Ξ£-pathp-dep refl $ transport (sym Squareβ‘double-composite-path) $ double-composite refl _ _ Β·Β· β-id-l _ Β·Β· ap (Ξ» e β lemmaβ x y e β Int.quot x y) (β€-prop (suc x) y x<y x<y') ... | inr (inl x>y) | inr (inl x>y') = Ξ£-pathp-dep refl $ Ξ£-pathp-dep refl $ transport (sym Squareβ‘double-composite-path) $ double-composite refl _ _ Β·Β· β-id-l _ Β·Β· ap (Ξ» e β lemmaβ x y e β Int.quot x y) (β€-prop (suc y) x x>y x>y') ... | inr (inr xβ‘y) | inr (inr xβ‘y') = Ξ£-pathp-dep refl $ Ξ£-pathp-dep refl $ transport (sym Squareβ‘double-composite-path) $ double-composite refl _ _ Β·Β· β-id-l _ Β·Β· ap (Ξ» e β lemmaβ x y e β Int.quot x y) (Nat-is-set _ _ _ _) -- 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 x>y) = absurd (go x y x<y x>y) where go : β x y β x < y β y < x β β₯ go (suc x) (suc y) p q = go x y p q ... | inl x<y | inr (inr xβ‘y) = absurd (go x y x<y (suc-inj xβ‘y)) where go : β x y β x < y β x β‘ y β β₯ go zero (suc y) p q = absurd (zeroβ suc q) go (suc x) (suc y) p q = go x y p (suc-inj q) ... | inr (inl x>y) | inl x<y = absurd (go x y x>y x<y) where go : β x y β y < x β x < y β β₯ go (suc x) (suc y) p q = go x y p q ... | inr (inr xβ‘y) | inl x<y = absurd (go x y x<y xβ‘y) where go : β x y β x < y β x β‘ y β β₯ go zero (suc y) p q = absurd (zeroβ suc q) go (suc x) (suc y) p q = go x y p (suc-inj q) ... | inr (inl x>y) | inr (inr xβ‘y) = absurd (go x y x>y (suc-inj xβ‘y)) where go : β x y β y < x β x β‘ y β β₯ go (suc x) zero p q = absurd (zeroβ suc (sym q)) go (suc x) (suc y) p q = go x y p (suc-inj q) ... | inr (inr xβ‘y) | inr (inl x>y) = absurd (go x y xβ‘y x>y) where go : β x y β x β‘ y β y < x β β₯ go (suc x) zero p q = absurd (zeroβ suc (sym p)) go (suc x) (suc y) p q = go x y (suc-inj p) q 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
$\bb{N} \times \bb{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 : \bb{Z} \to X$, it suffices to give a function $f : \bb{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' : \bb{Z}^2 \to X$
can be quite involved! It doesnβt suffice to exhibit a function from
$\bb{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(\id{S}a,\id{S}b,\id{S}x,\id{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

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:

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))

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
$\bb{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.

_*β€_ : 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)

In the diagram, we write $\id{S}x$ 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)$β©οΈ