open import 1Lab.Prelude

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

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) (s≀s p) = lemma₁ x y p βˆ™ Int.quot x y

  lemmaβ‚‚ (suc x) zero p          = refl
  lemmaβ‚‚ (suc x) (suc y) (s≀s 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 (s≀s 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) (≀-is-prop x<y x<y')
    ... | inr (inl x>y) | inr (inl (s≀s 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) (≀-is-prop 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 (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)

  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)β†©οΈŽ