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 N∐N\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) ⁣:N2(x , y)\colon \mathbb{N}^2 where (a,b)=(c,d)(a,b) = (c, d) iff a+d=b+ca + d = b + c: An integer is an equivalence class of pairs of naturals, where (a,b)(a, b) is identified with (1+a,1+b)(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)(a, b) = (1+a,1+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βˆ’nn - n is 00:

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)(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 nn and kk differ by an absolute value of bb, then the values nβˆ’kn - k and bb are the same (as long as we fix the sign β€” hence the two lemmas). The generic situation of β€œdiffering by bb” is captured by fixing a natural number aa and adding bb, because we have (a+b)βˆ’a=b(a + b) - a = b and aβˆ’(a+b)=βˆ’ba - (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             ∎

In the other direction, we must be clever: we use path induction, defining a type family Codea,b(x)\mathrm{Code}_{a,b}(x) such that the fibre of Codea,b\mathrm{Code}_{a,b} over (c,d)(c, d) is a+d=b+ca + 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+ma + n = b + m and a+1+n=b+1+ma + 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,ba, b, the family Codea,b(x)\mathrm{Code}_{a,b}(x) by recursion on the integer xx. Recall that we want the fibre over diff(c,d)\mathrm{diff}(c, d) to be a+d=b+ca + d = b + c, so that’s our pick. Now, the quot path constructor mandates that the fibre over (c,d)(c, d) be the same as that over (1+c,1+d)(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\mathrm{diff}(a, b) = x, we can apply path induction, whence it suffices to consider the case where xx is literally_ the difference of aa and bb. To lift this into our Code fibration, we must show that a+b=b+aa + b = b + a, but this is exactly commutativity of addition on N\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 N→N\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βˆ’ba-b. We split by cases:

  • If a<ba < b, then this is the same integer as 0βˆ’(bβˆ’a)0 - (b - a);
  • If a>ba > b, then this is the same integer as (aβˆ’b)βˆ’0(a - b) - 0;
  • If a=ba = b, then this is the same integer as 0βˆ’00 - 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\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:Z→Xf : \mathbb{Z} \to X, it suffices to give a function f:N2→Xf : \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 XX can be a more general space, not necessarily a set, defining a binary operation fβ€²:Z2β†’Xf' : \mathbb{Z}^2 \to X can be quite involved! It doesn’t suffice to exhibit a function from N4\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(Sa,Sb,Sx,Sy)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 XX1:

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 XX 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:

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)(a, b) is (1+a,b)(1 + a, b). Similarly, the predecessor of (a,b)(a, b) is (a,1+b)(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)(a, b) to (1+a,1+b)(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 xx has an additive inverse, denoted βˆ’x-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-x is an additive inverse to xx 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βˆ—yx*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\mathbb{Z} is a commutative ring.

The definition of multiplication is slightly tricky: We use the binomial theorem. Pretend that xyxy is really (aβˆ’b)(cβˆ’d)(a-b)(c-d), and expand that to (ac+bd)βˆ’(ad+bc)(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)
  *β„€-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 Sx\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)(0,1+x), (1+x,0)(1+x,0), or (0,0)(0,0)β†©οΈŽ