open import 1Lab.Prelude

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

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)

Warning

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) \sim (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 \to 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 \times 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 \to X,$ it suffices to give a function $f : 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^{'} : Z^{2} \to 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 (S a, S b, S x, 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$ ¹:

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 subtrahend², 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 $x y$ is really $(a - b) (c - d),$ and expand that to $(a c + b d) - (a d + b c) :$ 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 $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)$ ↩︎